Theorem had0OLD

Description: 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.)

	Ref	Expression
Assertion	had0OLD	$$⊢\neg \phi \to \left(hadd\left(\phi ,\psi ,\chi \right)\leftrightarrow \left(\psi ⊻\chi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		had1OLD	$$⊢\neg \phi \to \left(hadd\left(\neg \phi ,\neg \psi ,\neg \chi \right)\leftrightarrow \left(\neg \psi \leftrightarrow \neg \chi \right)\right)$$
2		hadnot	$$⊢\neg hadd\left(\phi ,\psi ,\chi \right)\leftrightarrow hadd\left(\neg \phi ,\neg \psi ,\neg \chi \right)$$
3		xnor	$$⊢\left(\psi \leftrightarrow \chi \right)\leftrightarrow \neg \left(\psi ⊻\chi \right)$$
4		notbi	$$⊢\left(\psi \leftrightarrow \chi \right)\leftrightarrow \left(\neg \psi \leftrightarrow \neg \chi \right)$$
5	3 4	bitr3i	$$⊢\neg \left(\psi ⊻\chi \right)\leftrightarrow \left(\neg \psi \leftrightarrow \neg \chi \right)$$
6	1 2 5	3bitr4g	$$⊢\neg \phi \to \left(\neg hadd\left(\phi ,\psi ,\chi \right)\leftrightarrow \neg \left(\psi ⊻\chi \right)\right)$$
7	6	con4bid	$$⊢\neg \phi \to \left(hadd\left(\phi ,\psi ,\chi \right)\leftrightarrow \left(\psi ⊻\chi \right)\right)$$