Metamath Proof Explorer

Theorem cadcoma

Description: Commutative law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016)

Ref Expression
Assertion cadcoma 
|- ( cadd ( ph , ps , ch ) <-> cadd ( ps , ph , ch ) )

Proof

Step Hyp Ref Expression
1 ancom 
 |-  ( ( ph /\ ps ) <-> ( ps /\ ph ) )
2 xorcom 
 |-  ( ( ph \/_ ps ) <-> ( ps \/_ ph ) )
3 2 anbi2i 
 |-  ( ( ch /\ ( ph \/_ ps ) ) <-> ( ch /\ ( ps \/_ ph ) ) )
4 1 3 orbi12i 
 |-  ( ( ( ph /\ ps ) \/ ( ch /\ ( ph \/_ ps ) ) ) <-> ( ( ps /\ ph ) \/ ( ch /\ ( ps \/_ ph ) ) ) )
5 df-cad 
 |-  ( cadd ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( ch /\ ( ph \/_ ps ) ) ) )
6 df-cad 
 |-  ( cadd ( ps , ph , ch ) <-> ( ( ps /\ ph ) \/ ( ch /\ ( ps \/_ ph ) ) ) )
7 4 5 6 3bitr4i 
 |-  ( cadd ( ph , ps , ch ) <-> cadd ( ps , ph , ch ) )