Theorem nancom

Alternative denial is commutative. Remark: alternative denial is not associative, see nanass. (Contributed by Mario Carneiro, 9-May-2015.) (Proof shortened by Wolf Lammen, 26-Jun-2020.)

Conclusion
\( \vdash \varphi \barwedge \psi \leftrightarrow \psi \barwedge \varphi \)
Proof
l0
con2b
\( \vdash \varphi \rightarrow \neg \psi \leftrightarrow \psi \rightarrow \neg \varphi \)
l1
dfnan2
\( \vdash \varphi \barwedge \psi \leftrightarrow \varphi \rightarrow \neg \psi \)
dfnan2
\( \vdash \psi \barwedge \varphi \leftrightarrow \psi \rightarrow \neg \varphi \)
3bitr4i l0 l1 _