Theorem hadcoma

Description: Commutative law for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 17-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		bicom	⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ( 𝜓 ↔ 𝜑 ) )
2	1	bibi1i	⊢ ( ( ( 𝜑 ↔ 𝜓 ) ↔ 𝜒 ) ↔ ( ( 𝜓 ↔ 𝜑 ) ↔ 𝜒 ) )
3		hadbi	⊢ ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ↔ 𝜓 ) ↔ 𝜒 ) )
4		hadbi	⊢ ( hadd ( 𝜓 , 𝜑 , 𝜒 ) ↔ ( ( 𝜓 ↔ 𝜑 ) ↔ 𝜒 ) )
5	2 3 4	3bitr4i	⊢ ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ hadd ( 𝜓 , 𝜑 , 𝜒 ) )