Theorem hadbi123d

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

	Ref	Expression
Hypotheses	hadbid.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
	hadbid.2	⊢ ( 𝜑 → ( 𝜃 ↔ 𝜏 ) )
	hadbid.3	⊢ ( 𝜑 → ( 𝜂 ↔ 𝜁 ) )
Assertion	hadbi123d	⊢ ( 𝜑 → ( hadd ( 𝜓 , 𝜃 , 𝜂 ) ↔ hadd ( 𝜒 , 𝜏 , 𝜁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hadbid.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
2		hadbid.2	⊢ ( 𝜑 → ( 𝜃 ↔ 𝜏 ) )
3		hadbid.3	⊢ ( 𝜑 → ( 𝜂 ↔ 𝜁 ) )
4	1 2	xorbi12d	⊢ ( 𝜑 → ( ( 𝜓 ⊻ 𝜃 ) ↔ ( 𝜒 ⊻ 𝜏 ) ) )
5	4 3	xorbi12d	⊢ ( 𝜑 → ( ( ( 𝜓 ⊻ 𝜃 ) ⊻ 𝜂 ) ↔ ( ( 𝜒 ⊻ 𝜏 ) ⊻ 𝜁 ) ) )
6		df-had	⊢ ( hadd ( 𝜓 , 𝜃 , 𝜂 ) ↔ ( ( 𝜓 ⊻ 𝜃 ) ⊻ 𝜂 ) )
7		df-had	⊢ ( hadd ( 𝜒 , 𝜏 , 𝜁 ) ↔ ( ( 𝜒 ⊻ 𝜏 ) ⊻ 𝜁 ) )
8	5 6 7	3bitr4g	⊢ ( 𝜑 → ( hadd ( 𝜓 , 𝜃 , 𝜂 ) ↔ hadd ( 𝜒 , 𝜏 , 𝜁 ) ) )