Theorem cadnot 1394

Description: The adder carry distributes over negation. (Contributed by Mario Carneiro, 4-Sep-2016.)

Assertion

Ref	Expression
cadnot	⊢ (¬ cadd(φ, ψ, χ) ↔ cadd(¬ φ, ¬ ψ, ¬ χ))

Proof of Theorem cadnot

Step	Hyp	Ref	Expression
1		3ioran 950	. . 3 ⊢ (¬ ((φ ∧ ψ) ∨ (φ ∧ χ) ∨ (ψ ∧ χ)) ↔ (¬ (φ ∧ ψ) ∧ ¬ (φ ∧ χ) ∧ ¬ (ψ ∧ χ)))
2		ianor 474	. . . 4 ⊢ (¬ (φ ∧ ψ) ↔ (¬ φ ∨ ¬ ψ))
3		ianor 474	. . . 4 ⊢ (¬ (φ ∧ χ) ↔ (¬ φ ∨ ¬ χ))
4		ianor 474	. . . 4 ⊢ (¬ (ψ ∧ χ) ↔ (¬ ψ ∨ ¬ χ))
5	2, 3, 4	3anbi123i 1140	. . 3 ⊢ ((¬ (φ ∧ ψ) ∧ ¬ (φ ∧ χ) ∧ ¬ (ψ ∧ χ)) ↔ ((¬ φ ∨ ¬ ψ) ∧ (¬ φ ∨ ¬ χ) ∧ (¬ ψ ∨ ¬ χ)))
6	1, 5	bitri 240	. 2 ⊢ (¬ ((φ ∧ ψ) ∨ (φ ∧ χ) ∨ (ψ ∧ χ)) ↔ ((¬ φ ∨ ¬ ψ) ∧ (¬ φ ∨ ¬ χ) ∧ (¬ ψ ∨ ¬ χ)))
7		cador 1391	. . 3 ⊢ (cadd(φ, ψ, χ) ↔ ((φ ∧ ψ) ∨ (φ ∧ χ) ∨ (ψ ∧ χ)))
8	7	notbii 287	. 2 ⊢ (¬ cadd(φ, ψ, χ) ↔ ¬ ((φ ∧ ψ) ∨ (φ ∧ χ) ∨ (ψ ∧ χ)))
9		cadan 1392	. 2 ⊢ (cadd(¬ φ, ¬ ψ, ¬ χ) ↔ ((¬ φ ∨ ¬ ψ) ∧ (¬ φ ∨ ¬ χ) ∧ (¬ ψ ∨ ¬ χ)))
10	6, 8, 9	3bitr4i 268	1 ⊢ (¬ cadd(φ, ψ, χ) ↔ cadd(¬ φ, ¬ ψ, ¬ χ))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 176   ∨ wo 357   ∧ wa 358   ∨ w3o 933   ∧ w3a 934  caddwcad 1379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-xor 1305  df-cad 1381

This theorem is used by: (None)