Theorem orbi12d

Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 21-Jun-1993.)

Hypotheses
bi12d.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
bi12d.2
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \tau) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \vee \theta \leftrightarrow \chi \vee \tau) \)
Proof
bi12d.1
l1
orbi1d _
\( \vdash \varphi \rightarrow (\psi \vee \theta \leftrightarrow \chi \vee \theta) \)
bi12d.2
orbi2d _
\( \vdash \varphi \rightarrow (\chi \vee \theta \leftrightarrow \chi \vee \tau) \)
bitrd l1 _