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 ) )