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