Theorem hadcomaOLD

Description: Obsolete version of hadcoma as of 17-Dec-2023. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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