Theorem
impcom
Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
Hypothesis
imp.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \psi \wedge \varphi \rightarrow \chi \)
Proof
imp.1
com12
_
imp
_
This is the content in the right pane.