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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notbi | ||
2 | 1 | bibi1i | |
3 | xor3 | ||
4 | hadbi | ||
5 | 3 4 | xchnxbir | |
6 | hadbi | ||
7 | 2 5 6 | 3bitr4i |