Theorem pm4.42

Theorem *4.42 of [WhiteheadRussell] p. 119. See also ifpid. (Contributed by Roy F. Longton, 21-Jun-2005.)

Conclusion
\( \vdash \varphi \leftrightarrow \varphi \wedge \psi \vee \varphi \wedge \neg \psi \)
Proof
l0
dedlema
\( \vdash \psi \rightarrow (\varphi \leftrightarrow \varphi \wedge \psi \vee \varphi \wedge \neg \psi) \)
dedlemb
\( \vdash \neg \psi \rightarrow (\varphi \leftrightarrow \varphi \wedge \psi \vee \varphi \wedge \neg \psi) \)
pm2.61i l0 _