Theorem
exp53
An exportation inference. (Contributed by Jeff Hankins, 30-Aug-2009.)
Hypothesis
exp53.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
exp53.1
ex
_
exp43
_
This is the content in the right pane.