Theorem pm5.7

Disjunction distributes over the biconditional. Theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbidi. (Contributed by Roy F. Longton, 21-Jun-2005.)

Conclusion
\( \vdash \varphi \vee \chi \leftrightarrow \psi \vee \chi \leftrightarrow \chi \vee (\varphi \leftrightarrow \psi) \)
Proof
l0
orbidi
\( \vdash \chi \vee (\varphi \leftrightarrow \psi) \leftrightarrow (\chi \vee \varphi \leftrightarrow \chi \vee \psi) \)
l1
orcom
orcom
bibi12i l1 _
\( \vdash \chi \vee \varphi \leftrightarrow \chi \vee \psi \leftrightarrow (\varphi \vee \chi \leftrightarrow \psi \vee \chi) \)
bitr2i l0 _