Theorem nanbi12i

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

Hypotheses
nanbii.1
\( \vdash \varphi \leftrightarrow \psi \)
nanbi12i.2
\( \vdash \chi \leftrightarrow \theta \)
Conclusion
\( \vdash \varphi \barwedge \chi \leftrightarrow \psi \barwedge \theta \)
Proof
l0
nanbii.1
\( \vdash \varphi \leftrightarrow \psi \)
l1
nanbi12i.2
\( \vdash \chi \leftrightarrow \theta \)
nanbi12
\( \vdash (\varphi \leftrightarrow \psi) \wedge (\chi \leftrightarrow \theta) \rightarrow (\varphi \barwedge \chi \leftrightarrow \psi \barwedge \theta) \)
mp2an l0 l1 _