Theorem orbi2i

Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.)

Hypothesis
orbi2i.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \chi \vee \varphi \leftrightarrow \chi \vee \psi \)
Proof
orbi2i.1
biimpi _
l2
orim2i _
orbi2i.1
biimpri _
orim2i _
impbii l2 _