Description: Commutative law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 11-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | cadcomb |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cadan | ||
2 | 3ancoma | ||
3 | orcom | ||
4 | 3 | 3anbi3i | |
5 | 1 2 4 | 3bitri | |
6 | cadan | ||
7 | 5 6 | bitr4i |