Theorem pm5.54

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

Conclusion
\( \vdash (\varphi \wedge \psi \leftrightarrow \varphi) \vee (\varphi \wedge \psi \leftrightarrow \psi) \)
Proof
iba
l1
bicomd _
adantl _
pm5.21ni _ l1
orri _