Theorem cadnot

Description: The adder carry distributes over negation. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 11-Jul-2020)

	Ref	Expression
Assertion	cadnot	$$⊢\neg cadd\left(\phi ,\psi ,\chi \right)\leftrightarrow cadd\left(\neg \phi ,\neg \psi ,\neg \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ianor	$$⊢\neg \left(\phi \wedge \psi \right)\leftrightarrow \left(\neg \phi \vee \neg \psi \right)$$
2		ianor	$$⊢\neg \left(\phi \wedge \chi \right)\leftrightarrow \left(\neg \phi \vee \neg \chi \right)$$
3		ianor	$$⊢\neg \left(\psi \wedge \chi \right)\leftrightarrow \left(\neg \psi \vee \neg \chi \right)$$
4	1 2 3	3anbi123i	$$⊢\left(\neg \left(\phi \wedge \psi \right)\wedge \neg \left(\phi \wedge \chi \right)\wedge \neg \left(\psi \wedge \chi \right)\right)\leftrightarrow \left(\left(\neg \phi \vee \neg \psi \right)\wedge \left(\neg \phi \vee \neg \chi \right)\wedge \left(\neg \psi \vee \neg \chi \right)\right)$$
5		3ioran	$$⊢\neg \left(\left(\phi \wedge \psi \right)\vee \left(\phi \wedge \chi \right)\vee \left(\psi \wedge \chi \right)\right)\leftrightarrow \left(\neg \left(\phi \wedge \psi \right)\wedge \neg \left(\phi \wedge \chi \right)\wedge \neg \left(\psi \wedge \chi \right)\right)$$
6		cador	$$⊢cadd\left(\phi ,\psi ,\chi \right)\leftrightarrow \left(\left(\phi \wedge \psi \right)\vee \left(\phi \wedge \chi \right)\vee \left(\psi \wedge \chi \right)\right)$$
7	5 6	xchnxbir	$$⊢\neg cadd\left(\phi ,\psi ,\chi \right)\leftrightarrow \left(\neg \left(\phi \wedge \psi \right)\wedge \neg \left(\phi \wedge \chi \right)\wedge \neg \left(\psi \wedge \chi \right)\right)$$
8		cadan	$$⊢cadd\left(\neg \phi ,\neg \psi ,\neg \chi \right)\leftrightarrow \left(\left(\neg \phi \vee \neg \psi \right)\wedge \left(\neg \phi \vee \neg \chi \right)\wedge \left(\neg \psi \vee \neg \chi \right)\right)$$
9	4 7 8	3bitr4i	$$⊢\neg cadd\left(\phi ,\psi ,\chi \right)\leftrightarrow cadd\left(\neg \phi ,\neg \psi ,\neg \chi \right)$$