Theorem pm4.54

Theorem *4.54 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.)

Conclusion
\( \vdash \neg \varphi \wedge \psi \leftrightarrow \neg (\varphi \vee \neg \psi) \)
Proof
l0
df-an
\( \vdash \neg \varphi \wedge \psi \leftrightarrow \neg (\neg \varphi \rightarrow \neg \psi) \)
pm4.66
\( \vdash \neg \varphi \rightarrow \neg \psi \leftrightarrow \varphi \vee \neg \psi \)
xchbinx l0 _