Theorem orbi1d

Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)

Hypothesis
bid.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \vee \theta \leftrightarrow \chi \vee \theta) \)
Proof
bid.1
l1
orbi2d _
\( \vdash \varphi \rightarrow (\theta \vee \psi \leftrightarrow \theta \vee \chi) \)
l2
orcom
\( \vdash \psi \vee \theta \leftrightarrow \theta \vee \psi \)
orcom
\( \vdash \chi \vee \theta \leftrightarrow \theta \vee \chi \)
3bitr4g l1 l2 _