Theorem orbi2d

Deduction adding a left 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 (\theta \vee \psi \leftrightarrow \theta \vee \chi) \)
Proof
bid.1
l1
imbi2d _
\( \vdash \varphi \rightarrow (\neg \theta \rightarrow \psi \leftrightarrow \neg \theta \rightarrow \chi) \)
l2
df-or
\( \vdash \theta \vee \psi \leftrightarrow \neg \theta \rightarrow \psi \)
df-or
\( \vdash \theta \vee \chi \leftrightarrow \neg \theta \rightarrow \chi \)
3bitr4g l1 l2 _