Theorem opeq1d 4807

Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)

Hypothesis

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

Assertion

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

Proof of Theorem opeq1d

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		opeq1 4801	. 2 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
3	1, 2	syl 17	1 ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   = wceq 1539  ⟨cop 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565

This theorem is referenced by:  oteq1  4810  oteq2  4811  opth  5385  elsnxp  6183  cbvoprab2  7341  fvproj  7946  unxpdomlem1  8956  djulf1o  9601  djurf1o  9602  mulcanenq  10647  ax1rid  10848  axrnegex  10849  fseq1m1p1  13260  uzrdglem  13605  pfxswrd  14347  swrdccat  14376  swrdccat3blem  14380  cshw0  14435  cshwmodn  14436  s2prop  14548  s4prop  14551  fsum2dlem  15410  fprod2dlem  15618  ruclem1  15868  imasaddvallem  17157  iscatd2  17307  moni  17365  homadmcd  17673  curf1  17859  curf1cl  17862  curf2  17863  hofcl  17893  gsum2dlem2  19487  imasdsf1olem  23434  ovoliunlem1  24571  cxpcn3  25806  axlowdimlem15  27227  axlowdim  27232  nvi  28877  nvop  28939  phop  29081  br8d  30851  fgreu  30911  1stpreimas  30940  smatfval  31647  smatrcl  31648  smatlem  31649  fmla0xp  33245  mvhfval  33395  mpst123  33402  br8  33629  frxp3  33724  xpord3pred  33725  nosupbnd2  33846  noinfbnd2  33861  fvtransport  34261  bj-inftyexpitaudisj  35303  rfovcnvf1od  41501