Metamath Proof Explorer


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 ¬ cadd φ ψ χ cadd ¬ φ ¬ ψ ¬ χ

Proof

Step Hyp Ref Expression
1 ianor ¬ φ ψ ¬ φ ¬ ψ
2 ianor ¬ φ χ ¬ φ ¬ χ
3 ianor ¬ ψ χ ¬ ψ ¬ χ
4 1 2 3 3anbi123i ¬ φ ψ ¬ φ χ ¬ ψ χ ¬ φ ¬ ψ ¬ φ ¬ χ ¬ ψ ¬ χ
5 3ioran ¬ φ ψ φ χ ψ χ ¬ φ ψ ¬ φ χ ¬ ψ χ
6 cador cadd φ ψ χ φ ψ φ χ ψ χ
7 5 6 xchnxbir ¬ cadd φ ψ χ ¬ φ ψ ¬ φ χ ¬ ψ χ
8 cadan cadd ¬ φ ¬ ψ ¬ χ ¬ φ ¬ ψ ¬ φ ¬ χ ¬ ψ ¬ χ
9 4 7 8 3bitr4i ¬ cadd φ ψ χ cadd ¬ φ ¬ ψ ¬ χ