Theorem pm5.63

Theorem *5.63 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)

Conclusion
\( \vdash \varphi \vee \psi \leftrightarrow \varphi \vee \neg \varphi \wedge \psi \)
Proof
l0
exmid
\( \vdash \varphi \vee \neg \varphi \)
ordi
\( \vdash \varphi \vee \neg \varphi \wedge \psi \leftrightarrow (\varphi \vee \neg \varphi) \wedge (\varphi \vee \psi) \)
mpbiran l0 _
bicomi _