Theorem hadnot 1393

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

Assertion

Ref	Expression
hadnot	⊢ (¬ hadd(φ, ψ, χ) ↔ hadd(¬ φ, ¬ ψ, ¬ χ))

Proof of Theorem hadnot

Step	Hyp	Ref	Expression
1		xorneg 1313	. . . 4 ⊢ ((¬ φ ⊻ ¬ ψ) ↔ (φ ⊻ ψ))
2		biid 227	. . . 4 ⊢ (¬ χ ↔ ¬ χ)
3	1, 2	xorbi12i 1314	. . 3 ⊢ (((¬ φ ⊻ ¬ ψ) ⊻ ¬ χ) ↔ ((φ ⊻ ψ) ⊻ ¬ χ))
4		xorneg2 1312	. . 3 ⊢ (((φ ⊻ ψ) ⊻ ¬ χ) ↔ ¬ ((φ ⊻ ψ) ⊻ χ))
5	3, 4	bitr2i 241	. 2 ⊢ (¬ ((φ ⊻ ψ) ⊻ χ) ↔ ((¬ φ ⊻ ¬ ψ) ⊻ ¬ χ))
6		df-had 1380	. . 3 ⊢ (hadd(φ, ψ, χ) ↔ ((φ ⊻ ψ) ⊻ χ))
7	6	notbii 287	. 2 ⊢ (¬ hadd(φ, ψ, χ) ↔ ¬ ((φ ⊻ ψ) ⊻ χ))
8		df-had 1380	. 2 ⊢ (hadd(¬ φ, ¬ ψ, ¬ χ) ↔ ((¬ φ ⊻ ¬ ψ) ⊻ ¬ χ))
9	5, 7, 8	3bitr4i 268	1 ⊢ (¬ hadd(φ, ψ, χ) ↔ hadd(¬ φ, ¬ ψ, ¬ χ))

Syntax hints:  ¬ wn 3   ↔ wb 176   ⊻ wxo 1304  haddwhad 1378

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-xor 1305  df-had 1380

This theorem is referenced by:  had0  1403