Theorem mpancom

An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses
mpancom.1
\( \vdash \psi \rightarrow \varphi \)
mpancom.2
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \psi \rightarrow \chi \)
Proof
l0
mpancom.1
\( \vdash \psi \rightarrow \varphi \)
l1
id
\( \vdash \psi \rightarrow \psi \)
mpancom.2
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
syl2anc l0 l1 _