Theorem oteq3d 4779

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

Hypothesis

Ref	Expression
oteq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
oteq3d	⊢ (𝜑 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)

Proof of Theorem oteq3d

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

Syntax hints:   → wi 4   = wceq 1538  ⟨cotp 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-ot 4534

This theorem is referenced by:  oteq123d  4780  idafval  17309  coafval  17316  arwlid  17324  arwrid  17325  arwass  17326  efgi  18837  efgtf  18840  efgtval  18841  efgval2  18842  mapdh6bN  39033  mapdh6cN  39034  mapdh6dN  39035  mapdh6gN  39038  hdmap1l6b  39107  hdmap1l6c  39108  hdmap1l6d  39109  hdmap1l6g  39112