Theorem nanbi12d

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

Hypotheses
nanbid.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
nanbi12d.2
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \tau) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \barwedge \theta \leftrightarrow \chi \barwedge \tau) \)
Proof
l0
nanbid.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
l1
nanbi12d.2
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \tau) \)
nanbi12
\( \vdash (\psi \leftrightarrow \chi) \wedge (\theta \leftrightarrow \tau) \rightarrow (\psi \barwedge \theta \leftrightarrow \chi \barwedge \tau) \)
syl2anc l0 l1 _