Theorem
exp5j
An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
Hypothesis
exp5j.1
\( \vdash \varphi \rightarrow \psi \wedge \chi \wedge \theta \wedge \tau \rightarrow \eta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \rightarrow \tau \rightarrow \eta \)
Proof
exp5j.1
expd
_
exp4c
_
This is the content in the right pane.