Theorem had0

Description: If the first input is false, then the adder sum is equivalent to the exclusive disjunction of the other two inputs. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 12-Jul-2020)

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

Proof

Step	Hyp	Ref	Expression
1		had1	$$⊢\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)$$