Theorem opeq2d 4176

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

Hypothesis

Ref	Expression
opeq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
opeq2d	|- ( ph -> <. C , A >. = <. C , B >. )

Proof of Theorem opeq2d

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 |- ( ph -> A = B )
2		opeq2 4170	. 2 |- ( A = B -> <. C , A >. = <. C , B >. )
3	1, 2	syl 17	1 |- ( ph -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   = wceq 1446   <.cop 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977

This theorem is referenced by:  fmptsng  6090  fmptsnd  6091  tfrlem11  7111  seqomlem0  7171  seqomlem1  7172  seqomlem4  7175  seqomeq12  7176  fundmen  7648  unxpdomlem1  7781  mulcanenq  9390  elreal2  9561  om2uzrdg  12177  uzrdgsuci  12181  seqeq2  12224  seqeq3  12225  s1val  12744  s1eq  12746  swrdlsw  12815  swrdccatwrd  12831  ccats1swrdeq  12832  ccatopth  12833  wrdeqcats1OLD  12837  swrdccat  12856  swrdccat3blem  12858  swrdccat3b  12859  swrdccatin12d  12864  splval  12865  splcl  12866  cshfn  12899  cshw0  12903  cshwmodn  12904  repswcshw  12918  swrds2  13032  swrd2lsw  13039  eucalgval  14553  setsidvald  15159  ressval  15188  ressress  15199  prdsval  15365  imasval  15423  imasvalOLD  15424  imasaddvallem  15447  cidval  15595  iscatd2  15599  oppcval  15630  ismon  15650  rescval  15744  idfucl  15798  funcres  15813  fucval  15875  fucpropd  15894  setcval  15984  catcval  16003  estrcval  16021  xpcval  16074  1stfcl  16094  2ndfcl  16095  curf12  16124  curf2val  16127  curfcl  16129  hofcl  16156  oduval  16388  ipoval  16412  frmdval  16647  oppgval  17010  symgval  17032  efgmval  17374  efgmnvl  17376  efgi  17381  frgpup3lem  17439  dprd2da  17687  dmdprdpr  17694  dprdpr  17695  pgpfaclem1  17726  mgpval  17738  mgpress  17746  opprval  17864  sraval  18411  rlmval2  18429  psrval  18598  opsrval  18710  opsrval2  18712  zlmval  19099  znval  19118  znval2  19120  thlval  19270  islindf4  19408  matval  19448  mat1dimmul  19513  mat1dimcrng  19514  mat1scmat  19576  mdet0pr  19629  m1detdiag  19634  txkgen  20679  pt1hmeo  20833  xpstopnlem1  20836  tusval  21293  tmsval  21508  tngval  21659  om1val  22073  pi1xfrcnvlem  22099  pi1xfrcnv  22100  dchrval  24174  ttgval  24917  eengv  25021  wwlkextwrd  25468  wwlkextproplem3  25483  clwlkisclwwlk2  25530  clwwlkf1  25536  clwlkfoclwwlk  25585  clwlkf1clwwlklem  25589  clwlkf1clwwlk  25590  clwlksizeeq  25592  eupath2lem3  25719  numclwlk1lem2f1  25834  numclwlk2lem2f1o  25845  br8d  28230  resvval  28602  smatfval  28633  smatrcl  28634  smatlem  28635  fvproj  28671  qqhval  28790  iwrdsplit  29232  bnj66  29683  bnj1234  29834  bnj1296  29842  bnj1450  29871  bnj1463  29876  bnj1501  29888  bnj1523  29892  subfacp1lem5  29919  cvmliftlem10  30029  cvmlift2lem12  30049  msubffval  30173  msubfval  30174  elmsubrn  30178  msubrn  30179  msubco  30181  br8  30408  br6  30409  btwnouttr2  30801  brfs  30858  btwnconn1lem11  30876  csbfinxpg  31792  finixpnum  31942  ldualset  32703  tgrpfset  34323  tgrpset  34324  erngfset  34378  erngset  34379  erngfset-rN  34386  erngset-rN  34387  dvafset  34583  dvaset  34584  dvhfset  34660  dvhset  34661  dvhfvadd  34671  dvhopvadd2  34674  dib1dim2  34748  dicvscacl  34771  cdlemn6  34782  dihopelvalcpre  34828  dih1dimatlem  34909  hdmapfval  35410  hlhilset  35517  mendval  36061  pfxpfx  38966  pfxccatin12d  38983  funopsn  39028  uspgr1ewop  39333  usgr2v1e2w  39337  idfusubc0  39969  idfusubc  39970  rngcvalALTV  40067  ringcvalALTV  40113  zlmodzxzsub  40245  lmod1zr  40390