Metamath Proof Explorer

Theorem hadass

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

Ref Expression
Assertion hadass 
|- ( hadd ( ph , ps , ch ) <-> ( ph \/_ ( ps \/_ ch ) ) )

Proof

Step Hyp Ref Expression
1 df-had 
 |-  ( hadd ( ph , ps , ch ) <-> ( ( ph \/_ ps ) \/_ ch ) )
2 xorass 
 |-  ( ( ( ph \/_ ps ) \/_ ch ) <-> ( ph \/_ ( ps \/_ ch ) ) )
3 1 2 bitri 
 |-  ( hadd ( ph , ps , ch ) <-> ( ph \/_ ( ps \/_ ch ) ) )