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 ( ¬ 𝜑 , ¬ 𝜓 , ¬ 𝜒 ) )