Theorem cadbi123d

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

	Ref	Expression
Hypotheses	cadbid.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
	cadbid.2	⊢ ( 𝜑 → ( 𝜃 ↔ 𝜏 ) )
	cadbid.3	⊢ ( 𝜑 → ( 𝜂 ↔ 𝜁 ) )
Assertion	cadbi123d	⊢ ( 𝜑 → ( cadd ( 𝜓 , 𝜃 , 𝜂 ) ↔ cadd ( 𝜒 , 𝜏 , 𝜁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cadbid.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
2		cadbid.2	⊢ ( 𝜑 → ( 𝜃 ↔ 𝜏 ) )
3		cadbid.3	⊢ ( 𝜑 → ( 𝜂 ↔ 𝜁 ) )
4	1 2	anbi12d	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜃 ) ↔ ( 𝜒 ∧ 𝜏 ) ) )
5	1 2	xorbi12d	⊢ ( 𝜑 → ( ( 𝜓 ⊻ 𝜃 ) ↔ ( 𝜒 ⊻ 𝜏 ) ) )
6	3 5	anbi12d	⊢ ( 𝜑 → ( ( 𝜂 ∧ ( 𝜓 ⊻ 𝜃 ) ) ↔ ( 𝜁 ∧ ( 𝜒 ⊻ 𝜏 ) ) ) )
7	4 6	orbi12d	⊢ ( 𝜑 → ( ( ( 𝜓 ∧ 𝜃 ) ∨ ( 𝜂 ∧ ( 𝜓 ⊻ 𝜃 ) ) ) ↔ ( ( 𝜒 ∧ 𝜏 ) ∨ ( 𝜁 ∧ ( 𝜒 ⊻ 𝜏 ) ) ) ) )
8		df-cad	⊢ ( cadd ( 𝜓 , 𝜃 , 𝜂 ) ↔ ( ( 𝜓 ∧ 𝜃 ) ∨ ( 𝜂 ∧ ( 𝜓 ⊻ 𝜃 ) ) ) )
9		df-cad	⊢ ( cadd ( 𝜒 , 𝜏 , 𝜁 ) ↔ ( ( 𝜒 ∧ 𝜏 ) ∨ ( 𝜁 ∧ ( 𝜒 ⊻ 𝜏 ) ) ) )
10	7 8 9	3bitr4g	⊢ ( 𝜑 → ( cadd ( 𝜓 , 𝜃 , 𝜂 ) ↔ cadd ( 𝜒 , 𝜏 , 𝜁 ) ) )