Theorem oteq1

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

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

Proof

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