Theorem com12

Inference that swaps (commutes) antecedents in an implication. Inference associated with pm2.04. Its associated inference is mpi. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)

Hypothesis
com12.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \psi \rightarrow \varphi \rightarrow \chi \)
Proof
l0
id
\( \vdash \psi \rightarrow \psi \)
com12.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syl5com l0 _