Theorem biancomd

Commuting conjunction in a biconditional, deduction form. (Contributed by Peter Mazsa, 3-Oct-2018.)

Hypothesis
biancomd.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \theta \wedge \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi \wedge \theta) \)
Proof
l0
biancomd.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \theta \wedge \chi) \)
ancom
\( \vdash \theta \wedge \chi \leftrightarrow \chi \wedge \theta \)
bitrdi l0 _