Theorem oteq3

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

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

Proof

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