Theorem pm5.62

Theorem *5.62 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 21-Jun-2005.)

Conclusion
\( \vdash \varphi \wedge \psi \vee \neg \psi \leftrightarrow \varphi \vee \neg \psi \)
Proof
l0
exmid
\( \vdash \psi \vee \neg \psi \)
ordir
\( \vdash \varphi \wedge \psi \vee \neg \psi \leftrightarrow (\varphi \vee \neg \psi) \wedge (\psi \vee \neg \psi) \)
mpbiran2 l0 _