Metamath Proof Explorer


Theorem cadrot

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

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

Proof

Step Hyp Ref Expression
1 cadcoma
 |-  ( cadd ( ph , ps , ch ) <-> cadd ( ps , ph , ch ) )
2 cadcomb
 |-  ( cadd ( ps , ph , ch ) <-> cadd ( ps , ch , ph ) )
3 1 2 bitri
 |-  ( cadd ( ph , ps , ch ) <-> cadd ( ps , ch , ph ) )