Theorem bi2.04

Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 11-May-1993.)

Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \leftrightarrow \psi \rightarrow \varphi \rightarrow \chi \)
Proof
l0
pm2.04
pm2.04
impbii l0 _