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