Theorem mpcom

Modus ponens inference with commutation of antecedents. Commuted form of mpd. (Contributed by NM, 17-Mar-1996.)

Hypotheses
mpcom.1
\( \vdash \psi \rightarrow \varphi \)
mpcom.2
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \psi \rightarrow \chi \)
Proof
l0
mpcom.1
\( \vdash \psi \rightarrow \varphi \)
mpcom.2
com12 _
\( \vdash \psi \rightarrow \varphi \rightarrow \chi \)
mpd l0 _