Theorem nanor

Alternative denial in terms of disjunction and negation. This explains the name "alternative denial". (Contributed by BJ, 19-Oct-2022.)

Conclusion
\( \vdash \varphi \barwedge \psi \leftrightarrow \neg \varphi \vee \neg \psi \)
Proof
l0
df-nan
\( \vdash \varphi \barwedge \psi \leftrightarrow \neg (\varphi \wedge \psi) \)
ianor
\( \vdash \neg (\varphi \wedge \psi) \leftrightarrow \neg \varphi \vee \neg \psi \)
bitri l0 _