Theorem
exp516
A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
Hypothesis
exp516.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
exp516.1
exp31
_
3expd
_
This is the content in the right pane.