Theorem pm5.61

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

Conclusion
\( \vdash (\varphi \vee \psi) \wedge \neg \psi \leftrightarrow \varphi \wedge \neg \psi \)
Proof
l0
orel2
orc
impbid1 l0 _
pm5.32ri _