Theorem pm5.15

Theorem *5.15 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 15-Oct-2013.)

Conclusion
\( \vdash (\varphi \leftrightarrow \psi) \vee (\varphi \leftrightarrow \neg \psi) \)
Proof
xor3
biimpi _
orri _