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