Theorem anbi1cd

Introduce a proposition as left conjunct on the left-hand side and right conjunct on the right-hand side of an equivalence. Deduction form. (Contributed by Peter Mazsa, 22-May-2021.)

Hypothesis

anbi1cd.1

\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)

Conclusion

\( \vdash \varphi \rightarrow (\theta \wedge \psi \leftrightarrow \chi \wedge \theta) \)

Proof

anbi1cd.1

anbi2d _

biancomd _