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