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