Theorem orbi1i

Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.)

Hypothesis
orbi2i.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \varphi \vee \chi \leftrightarrow \psi \vee \chi \)
Proof
l0
orcom
\( \vdash \varphi \vee \chi \leftrightarrow \chi \vee \varphi \)
orbi2i.1
l2
orbi2i _
\( \vdash \chi \vee \varphi \leftrightarrow \chi \vee \psi \)
orcom
\( \vdash \chi \vee \psi \leftrightarrow \psi \vee \chi \)
3bitri l0 l2 _