Theorem nanbi12

Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.)

Conclusion
\( \vdash (\varphi \leftrightarrow \psi) \wedge (\chi \leftrightarrow \theta) \rightarrow (\varphi \barwedge \chi \leftrightarrow \psi \barwedge \theta) \)
Proof
l0
nanbi1
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow (\varphi \barwedge \chi \leftrightarrow \psi \barwedge \chi) \)
nanbi2
\( \vdash (\chi \leftrightarrow \theta) \rightarrow (\psi \barwedge \chi \leftrightarrow \psi \barwedge \theta) \)
sylan9bb l0 _