Theorem had0OLD

Obsolete version of had0 as of 10-Aug-2026. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 12-Jul-2020.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \neg \varphi \rightarrow (\text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow \psi \veebar \chi) \)
Proof
l0
had1OLD
\( \vdash \neg \varphi \rightarrow (\text{ hadd } ( \neg \varphi , \neg \psi , \neg \chi ) \leftrightarrow (\neg \psi \leftrightarrow \neg \chi)) \)
l1
hadnot
\( \vdash \neg \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow \text{ hadd } ( \neg \varphi , \neg \psi , \neg \chi ) \)
l2
xnor
\( \vdash \psi \leftrightarrow \chi \leftrightarrow \neg (\psi \veebar \chi) \)
notbi
\( \vdash \psi \leftrightarrow \chi \leftrightarrow (\neg \psi \leftrightarrow \neg \chi) \)
bitr3i l2 _
\( \vdash \neg (\psi \veebar \chi) \leftrightarrow (\neg \psi \leftrightarrow \neg \chi) \)
3bitr4g l0 l1 _
con4bid _