Theorem orbi12i

Infer the disjunction of two equivalences. (Contributed by NM, 3-Jan-1993.)

Hypotheses
orbi12i.1
\( \vdash \varphi \leftrightarrow \psi \)
orbi12i.2
\( \vdash \chi \leftrightarrow \theta \)
Conclusion
\( \vdash \varphi \vee \chi \leftrightarrow \psi \vee \theta \)
Proof
orbi12i.2
l1
orbi2i _
\( \vdash \varphi \vee \chi \leftrightarrow \varphi \vee \theta \)
orbi12i.1
orbi1i _
\( \vdash \varphi \vee \theta \leftrightarrow \psi \vee \theta \)
bitri l1 _