Metamath Proof Explorer


Theorem hadnot

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

Ref Expression
Assertion hadnot ¬ hadd φ ψ χ hadd ¬ φ ¬ ψ ¬ χ

Proof

Step Hyp Ref Expression
1 notbi φ ψ ¬ φ ¬ ψ
2 1 bibi1i φ ψ ¬ χ ¬ φ ¬ ψ ¬ χ
3 xor3 ¬ φ ψ χ φ ψ ¬ χ
4 hadbi hadd φ ψ χ φ ψ χ
5 3 4 xchnxbir ¬ hadd φ ψ χ φ ψ ¬ χ
6 hadbi hadd ¬ φ ¬ ψ ¬ χ ¬ φ ¬ ψ ¬ χ
7 2 5 6 3bitr4i ¬ hadd φ ψ χ hadd ¬ φ ¬ ψ ¬ χ