Theorem pm5.55

Theorem *5.55 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 20-Jan-2013.)

Conclusion
\( \vdash (\varphi \vee \psi \leftrightarrow \varphi) \vee (\varphi \vee \psi \leftrightarrow \psi) \)
Proof
biort
l1
bicomd _
\( \vdash \varphi \rightarrow (\varphi \vee \psi \leftrightarrow \varphi) \)
biorf
bicomd _
\( \vdash \neg \varphi \rightarrow (\varphi \vee \psi \leftrightarrow \psi) \)
nsyl5 l1 _
orri _