Theorem opeq1d 4812

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

Syntax hints:   → wi 4   = wceq 1536  ⟨cop 4576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577

This theorem is referenced by:  oteq1  4815  oteq2  4816  opth  5371  elsnxp  6145  cbvoprab2  7245  fvproj  7831  unxpdomlem1  8725  djulf1o  9344  djurf1o  9345  mulcanenq  10385  ax1rid  10586  axrnegex  10587  fseq1m1p1  12985  uzrdglem  13328  pfxswrd  14071  swrdccat  14100  swrdccat3blem  14104  cshw0  14159  cshwmodn  14160  s2prop  14272  s4prop  14275  fsum2dlem  15128  fprod2dlem  15337  ruclem1  15587  imasaddvallem  16805  iscatd2  16955  moni  17009  homadmcd  17305  curf1  17478  curf1cl  17481  curf2  17482  hofcl  17512  gsum2dlem2  19094  imasdsf1olem  22986  ovoliunlem1  24106  cxpcn3  25332  axlowdimlem15  26745  axlowdim  26750  nvi  28394  nvop  28456  phop  28598  br8d  30364  fgreu  30420  1stpreimas  30444  smatfval  31064  smatrcl  31065  smatlem  31066  fmla0xp  32634  mvhfval  32784  mpst123  32791  br8  32996  nosupbnd2  33220  fvtransport  33497  bj-inftyexpitaudisj  34491  rfovcnvf1od  40356