Theorem hadcomb

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

	Ref	Expression
Assertion	hadcomb	⊢ ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ hadd ( 𝜑 , 𝜒 , 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		biid	⊢ ( 𝜑 ↔ 𝜑 )
2		xorcom	⊢ ( ( 𝜓 ⊻ 𝜒 ) ↔ ( 𝜒 ⊻ 𝜓 ) )
3	1 2	xorbi12i	⊢ ( ( 𝜑 ⊻ ( 𝜓 ⊻ 𝜒 ) ) ↔ ( 𝜑 ⊻ ( 𝜒 ⊻ 𝜓 ) ) )
4		hadass	⊢ ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑 ⊻ ( 𝜓 ⊻ 𝜒 ) ) )
5		hadass	⊢ ( hadd ( 𝜑 , 𝜒 , 𝜓 ) ↔ ( 𝜑 ⊻ ( 𝜒 ⊻ 𝜓 ) ) )
6	3 4 5	3bitr4i	⊢ ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ hadd ( 𝜑 , 𝜒 , 𝜓 ) )