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