Metamath Proof Explorer


Theorem oteq2d

Description: Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypothesis oteq1d.1 ( 𝜑𝐴 = 𝐵 )
Assertion oteq2d ( 𝜑 → ⟨ 𝐶 , 𝐴 , 𝐷 ⟩ = ⟨ 𝐶 , 𝐵 , 𝐷 ⟩ )

Proof

Step Hyp Ref Expression
1 oteq1d.1 ( 𝜑𝐴 = 𝐵 )
2 oteq2 ( 𝐴 = 𝐵 → ⟨ 𝐶 , 𝐴 , 𝐷 ⟩ = ⟨ 𝐶 , 𝐵 , 𝐷 ⟩ )
3 1 2 syl ( 𝜑 → ⟨ 𝐶 , 𝐴 , 𝐷 ⟩ = ⟨ 𝐶 , 𝐵 , 𝐷 ⟩ )