Theorem oteq3d 4819

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 4816	. 2 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)
3	1, 2	syl 17	1 ⊢ (𝜑 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)

Syntax hints:   → wi 4   = wceq 1537  ⟨cotp 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-ot 4578

This theorem is referenced by:  oteq123d  4820  idafval  17319  coafval  17326  arwlid  17334  arwrid  17335  arwass  17336  efgi  18847  efgtf  18850  efgtval  18851  efgval2  18852  mapdh6bN  38875  mapdh6cN  38876  mapdh6dN  38877  mapdh6gN  38880  hdmap1l6b  38949  hdmap1l6c  38950  hdmap1l6d  38951  hdmap1l6g  38954