Metamath Proof Explorer

Theorem hadrot

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

Ref Expression
Assertion hadrot 
|- ( hadd ( ph , ps , ch ) <-> hadd ( ps , ch , ph ) )

Proof

Step Hyp Ref Expression
1 hadcoma 
 |-  ( hadd ( ph , ps , ch ) <-> hadd ( ps , ph , ch ) )
2 hadcomb 
 |-  ( hadd ( ps , ph , ch ) <-> hadd ( ps , ch , ph ) )
3 1 2 bitri 
 |-  ( hadd ( ph , ps , ch ) <-> hadd ( ps , ch , ph ) )