Metamath Proof Explorer

Theorem cadcomb

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 
|- ( cadd ( ph , ps , ch ) <-> cadd ( ph , ch , ps ) )

Proof

Step Hyp Ref Expression
1 cadan 
 |-  ( cadd ( ph , ps , ch ) <-> ( ( ph \/ ps ) /\ ( ph \/ ch ) /\ ( ps \/ ch ) ) )
2 3ancoma 
 |-  ( ( ( ph \/ ps ) /\ ( ph \/ ch ) /\ ( ps \/ ch ) ) <-> ( ( ph \/ ch ) /\ ( ph \/ ps ) /\ ( ps \/ ch ) ) )
3 orcom 
 |-  ( ( ps \/ ch ) <-> ( ch \/ ps ) )
4 3 3anbi3i 
 |-  ( ( ( ph \/ ch ) /\ ( ph \/ ps ) /\ ( ps \/ ch ) ) <-> ( ( ph \/ ch ) /\ ( ph \/ ps ) /\ ( ch \/ ps ) ) )
5 1 2 4 3bitri 
 |-  ( cadd ( ph , ps , ch ) <-> ( ( ph \/ ch ) /\ ( ph \/ ps ) /\ ( ch \/ ps ) ) )
6 cadan 
 |-  ( cadd ( ph , ch , ps ) <-> ( ( ph \/ ch ) /\ ( ph \/ ps ) /\ ( ch \/ ps ) ) )
7 5 6 bitr4i 
 |-  ( cadd ( ph , ps , ch ) <-> cadd ( ph , ch , ps ) )