Theorem oteq2

Description: Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015)

	Ref	Expression
Assertion	oteq2	⊢ ( 𝐴 = 𝐵 → ⟨ 𝐶 , 𝐴 , 𝐷 ⟩ = ⟨ 𝐶 , 𝐵 , 𝐷 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		opeq2	⊢ ( 𝐴 = 𝐵 → ⟨ 𝐶 , 𝐴 ⟩ = ⟨ 𝐶 , 𝐵 ⟩ )
2	1	opeq1d	⊢ ( 𝐴 = 𝐵 → ⟨ ⟨ 𝐶 , 𝐴 ⟩ , 𝐷 ⟩ = ⟨ ⟨ 𝐶 , 𝐵 ⟩ , 𝐷 ⟩ )
3		df-ot	⊢ ⟨ 𝐶 , 𝐴 , 𝐷 ⟩ = ⟨ ⟨ 𝐶 , 𝐴 ⟩ , 𝐷 ⟩
4		df-ot	⊢ ⟨ 𝐶 , 𝐵 , 𝐷 ⟩ = ⟨ ⟨ 𝐶 , 𝐵 ⟩ , 𝐷 ⟩
5	2 3 4	3eqtr4g	⊢ ( 𝐴 = 𝐵 → ⟨ 𝐶 , 𝐴 , 𝐷 ⟩ = ⟨ 𝐶 , 𝐵 , 𝐷 ⟩ )