Theorem
exp520
A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
Hypothesis
exp520.1
\( \vdash (\varphi \wedge \psi \wedge \chi) \wedge (\theta \wedge \tau) \rightarrow \eta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \rightarrow \tau \rightarrow \eta \)
Proof
exp520.1
ex
_
exp5o
_
This is the content in the right pane.