Metamath Proof Explorer


Theorem hadcomb

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

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

Proof

Step Hyp Ref Expression
1 biid
 |-  ( ph <-> ph )
2 xorcom
 |-  ( ( ps \/_ ch ) <-> ( ch \/_ ps ) )
3 1 2 xorbi12i
 |-  ( ( ph \/_ ( ps \/_ ch ) ) <-> ( ph \/_ ( ch \/_ ps ) ) )
4 hadass
 |-  ( hadd ( ph , ps , ch ) <-> ( ph \/_ ( ps \/_ ch ) ) )
5 hadass
 |-  ( hadd ( ph , ch , ps ) <-> ( ph \/_ ( ch \/_ ps ) ) )
6 3 4 5 3bitr4i
 |-  ( hadd ( ph , ps , ch ) <-> hadd ( ph , ch , ps ) )