Theorem ancomd

Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.)

Hypothesis
ancomd.1
\( \vdash \varphi \rightarrow \psi \wedge \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \wedge \psi \)
Proof
l0
ancomd.1
\( \vdash \varphi \rightarrow \psi \wedge \chi \)
ancom
\( \vdash \psi \wedge \chi \leftrightarrow \chi \wedge \psi \)
sylib l0 _