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