Theorem 3eqtr4g 2510

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
3eqtr4g.1	|- ( ph -> A = B )
3eqtr4g.2	|- C = A
3eqtr4g.3	|- D = B

Assertion

Ref	Expression
3eqtr4g	|- ( ph -> C = D )

Proof of Theorem 3eqtr4g

Step	Hyp	Ref	Expression
1		3eqtr4g.2	. . 3 |- C = A
2		3eqtr4g.1	. . 3 |- ( ph -> A = B )
3	1, 2	syl5eq 2497	. 2 |- ( ph -> C = B )
4		3eqtr4g.3	. 2 |- D = B
5	3, 4	syl6eqr 2503	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-cleq 2444

This theorem is referenced by:  rabbidva2  3034  rabeqf  3037  csbeq1  3366  csbeq2  3367  difeq1  3544  difeq2  3545  uneq2  3582  ineq2  3628  symdifeq1  3665  symdifeq2  3666  dfrab3ss  3721  csbeq2d  3780  csbnestgf  3785  ifeq1  3885  ifeq2  3886  pweq  3954  sneq  3978  csbsng  4030  csbprg  4031  rabsn  4039  preq1  4051  preq2  4052  tpeq1  4060  tpeq2  4061  tpeq3  4062  prprc1  4082  opeq1  4166  opeq2  4167  oteq1  4175  oteq2  4176  oteq3  4177  unieq  4206  csbuni  4226  inteq  4237  iineq1  4293  iineq2  4296  dfiin2g  4311  iinrab  4340  iinin1  4349  iinxprg  4359  iununi  4366  opabbid  4465  mpteq12f  4479  csbmpt12  4735  xpeq1  4848  xpeq2  4849  rneq  5060  reseq1  5099  reseq2  5100  resmpt  5154  imaeq1  5163  imaeq2  5164  mptcnv  5238  dmpropg  5309  rnpropg  5316  cores  5338  cores2  5348  xpco  5376  predeq123  5381  suceq  5488  iotaeq  5554  iotabi  5555  fntpg  5637  imain  5659  f1oprswap  5854  fveq1  5864  fveq2  5865  fvres  5879  csbfv12  5900  fnimapr  5929  fvco2  5940  residpr  6068  fsnunfv  6104  fsnunres  6105  funiunfv  6153  fliftf  6208  isoini2  6230  riotaeqdv  6253  riotabidv  6254  riotauni  6258  riotabidva  6268  snriota  6281  oveq  6296  oveq1  6297  oveq2  6298  oprabbid  6344  mpt2eq123  6350  mpt2eq123dva  6352  mpt2eq3dva  6355  resmpt2  6394  ovres  6436  f1ocnvd  6518  ofeq  6533  ofreq  6534  fpar  6900  wrecseq123  7029  onovuni  7061  recseq  7092  tfr2a  7113  rdgeq1  7129  rdgeq2  7130  rdgsucmptf  7146  frsucmpt  7155  seqomeq12  7171  seqomsuc  7174  omopthi  7358  eceq1  7399  eceq2  7401  qseq1  7413  qseq2  7414  uniqs  7423  ecinxp  7438  qsinxp  7439  erovlem  7459  ecopovtrn  7466  ixpeq1  7533  supeq1  7959  supeq2  7962  supeq3  7963  supeq123d  7964  infeq1  7992  infeq2  7995  infeq3  7996  infeq123d  7997  infiso  8023  oieq1  8027  oieq2  8028  ordtypelem1  8033  inf3lemc  8131  wemapwe  8202  r1sucg  8240  r1limg  8242  rankprb  8322  karden  8366  cardiun  8416  acneq  8474  alephlim  8498  alephsuc  8499  alephfplem2  8536  infpssrlem2  8734  fin23lem34  8776  fin23lem35  8777  zorn2lem1  8926  zorn2lem7  8932  fpwwe2lem6  9060  fpwwe2lem13  9067  addpiord  9309  mulpiord  9310  addpqnq  9363  mulpqnq  9366  addassnq  9383  mulassnq  9384  distrnq  9386  lterpq  9395  ltexnq  9400  ltsrpr  9501  00sr  9523  recexsrlem  9527  mulgt0sr  9529  addcnsrec  9567  mulcnsrec  9568  negeq  9867  csbnegg  9872  negsubdi  9930  mulneg1  10055  negfi  10554  deceq1  11054  deceq2  11055  xnegeq  11500  fseq1p1m1  11868  om2uzrdg  12170  uzrdgsuci  12174  seqeq1  12216  seqeq2  12217  seqeq3  12218  seqfeq4  12262  seqof  12270  hashprg  12572  hashmap  12607  hashtpg  12641  csbwrdg  12696  s1eq  12739  cats1co  12952  s2eqd  12958  s3eqd  12959  s4eqd  12960  s5eqd  12961  s6eqd  12962  s7eqd  12963  s8eqd  12964  xpcogend  13038  shftval  13137  limsupgle  13535  lo1eq  13632  rlimeq  13633  sumeq1  13755  sumeq2w  13758  sumeq2ii  13759  zsum  13784  sumss2  13792  fsumsplitsnun  13816  isumclim3  13820  fsumcom2  13835  incexclem  13894  incexc2  13896  isumshft  13897  prodeq1f  13962  prodeq2w  13966  prodeq2ii  13967  zprod  13991  fprodm1s  14024  fprodp1s  14025  fprodcom2  14038  iprodclim3  14053  ef0lem  14133  ruclem7  14288  sadcp1  14429  smupp1  14454  smueqlem  14464  algrp1  14533  dfphi2  14722  prmdiveq  14734  pceulem  14795  vdwlem6  14936  cshwsiun  15070  setsid  15164  elbasfv  15170  elbasov  15171  imastset  15423  imasvscaval  15444  xpscg  15464  isoval  15670  funcoppc  15780  fulloppc  15827  fuccofval  15864  natpropd  15881  catccofval  15995  xpchomfval  16064  xpccofval  16067  lubfval  16224  glbfval  16237  grpidpropd  16504  gsumpropd2lem  16516  frmdplusg  16638  grpinvpropd  16729  grpsubpropd  16756  grpsubpropd2  16757  mulgpropd  16791  oppgmnd  17005  symgplusg  17030  sylow1lem2  17251  sylow3lem1  17279  prds1  17842  pwsmgp  17846  opprring  17859  rngidpropd  17923  dvdsrpropd  17924  unitpropd  17925  invrpropd  17926  rhm1  17958  lmhmpropd  18296  lidlrsppropd  18454  lpival  18469  ressascl  18568  asclpropd  18570  aspval2  18571  psrbas  18602  psrplusg  18605  psrmulr  18608  psrvscafval  18614  resspsrbas  18639  ressmplbas2  18679  opsrle  18699  opsrbaslem  18701  vr1val  18785  ressply1add  18823  ressply1mul  18824  ressply1vsca  18825  psrplusgpropd  18829  mplbaspropd  18830  psropprmul  18831  ply1baspropd  18836  ply1plusgpropd  18837  ply1sca2  18847  subrgvr1  18854  coe1mul2lem2  18861  ply1coe1eq  18892  zrhpropd  19086  znle  19107  frlmplusgval  19326  frlmvscafval  19328  mamudi  19428  mamudir  19429  matrcl  19437  oftpos  19477  mattpos1  19481  mdetfval  19611  mdetrlin  19627  mdetrsca  19628  mdetrsca2  19629  mdetrlin2  19632  mdetunilem5  19641  madufval  19662  madugsum  19668  idmatidpmat  19761  cpmidpmat  19897  cncmp  20407  2ndcsep  20474  llyeq  20485  nllyeq  20486  xkouni  20614  hmphindis  20812  xkocnv  20829  ptcmplem2  21068  snclseqg  21130  prdstmdd  21138  ustexsym  21230  ucnextcn  21319  metreslem  21377  comet  21528  nrmmetd  21589  nmpropd  21608  isngp3  21612  ngpds  21617  subgnm  21641  tngnm  21659  idnghm  21764  cnmetdval  21791  cnmpt2pc  21956  htpyco2  22010  phtpyco2  22021  clsocv  22221  rrxprds  22348  rrxnm  22350  ovolunlem1a  22449  voliunlem3  22505  ioombl1lem4  22514  uniioombllem4  22544  itg11  22649  itgeq1f  22729  itgeq2  22735  iblss2  22763  itgss  22769  itgeqa  22771  itgfsum  22784  itgsplit  22793  ditgeq1  22803  ditgeq2  22804  ditgeq3  22805  dvcmulf  22899  dvmptfsum  22927  dvcnvrelem2  22970  mdegfval  23011  mdegpropd  23033  deg1propd  23035  plyeq0  23165  coe11  23207  dgrlt  23220  dgradd2  23222  dgrmulc  23225  dvply1  23237  fta1lem  23260  pserulm  23377  rlimcnp2  23892  jensenlem1  23912  basellem5  24011  dchrbas  24163  dchrrcl  24168  dchrplusg  24175  dchrfi  24183  lgsdi  24260  lgseisenlem2  24278  lgsquadlem3  24284  dchrmusumlema  24331  rpvmasum2  24350  dchrisum0lema  24352  pntlemg  24436  colperpexlem2  24773  axlowdimlem13  24984  nbgraf1olem5  25173  nb3graprlem1  25179  constr2spthlem1  25324  constr3pthlem1  25383  constr3pthlem2  25384  avril1  25900  0vfval  26225  imsval  26317  imsdval  26318  bcseqi  26773  normpythi  26795  cm0  27262  fh1  27271  pjcji  27337  opsqrlem5  27797  pjsdi2i  27810  pjclem3  27850  pjci  27853  golem1  27924  iunrdx  28179  ofresid  28243  mpteq12df  28256  resmptf  28257  f1od2  28309  gsumvsca1  28545  gsumvsca2  28546  rhmopp  28582  resv1r  28600  fzto1st1  28615  crefeq  28672  xrge0mulc1cn  28747  qqhval2  28786  esumeq12dvaf  28852  esumeq2  28857  esumf1o  28871  esumfzf  28890  esumss  28893  esumpfinvalf  28897  ofceq  28918  itgeq12dv  29159  ccatmulgnn0dir  29428  bnj956  29588  bnj1385  29644  bnj96  29676  bnj548  29708  bnj553  29709  bnj554  29710  bnj602  29726  bnj18eq1  29738  bnj1234  29822  bnj1296  29830  bnj1318  29834  bnj1442  29858  bnj1450  29859  cvmliftlem5  30012  cvmliftlem10  30017  cvmlift2lem9  30034  cvmliftphtlem  30040  mthmpps  30220  mpteq12d  30412  rdgprc  30441  dfrdg2  30442  trpredeq1  30461  trpredeq2  30462  trpredeq3  30463  wsuceq123  30497  wlimeq12  30502  altopthsn  30728  altxpeq1  30740  altxpeq2  30741  ee7.2aOLD  31121  bj-rabbida2  31520  bj-sngleq  31561  bj-tageq  31570  bj-projeq  31586  bj-projval  31590  bj-1upleq  31593  bj-pr1eq  31596  bj-pr2eq  31610  csbopg2  31725  csbpredg  31727  csbwrecsg  31728  csbrecsg  31729  csbrdgg  31730  csboprabg  31731  csbmpt22g  31732  finxpeq1  31778  finxpeq2  31779  csbfinxpg  31780  finxpreclem4  31786  finixpnum  31930  ptrest  31939  poimirlem3  31943  poimirlem9  31949  poimirlem15  31955  poimirlem16  31956  poimirlem26  31966  poimirlem27  31967  mbfposadd  31988  cnambfre  31989  iblabsnclem  32005  ftc1anclem1  32017  heiborlem4  32146  heiborlem6  32148  mpt2bi123f  32406  iineq12f  32408  mptbi12f  32410  riotaclbgBAD  32526  toycom  32539  ldualvbase  32692  ldualfvadd  32694  ldualsca  32698  ldualsbase  32699  ldualsaddN  32700  ldualfvs  32702  ldual0  32713  ldual1  32714  ldualneg  32715  cdleme19f  33875  cdleme20m  33890  cdleme21k  33905  cdleme27b  33935  cdleme31so  33946  cdleme31sn  33947  cdleme31se  33949  cdleme31se2  33950  cdleme31sc  33951  cdleme31sde  33952  cdleme31fv  33957  cdleme40v  34036  cdleme43dN  34059  cdlemeg46ngfr  34085  ltrnco4  34306  tgrpbase  34313  tgrpopr  34314  erngbase  34368  erngfplus  34369  erngfmul  34372  erngbase-rN  34376  erngfplus-rN  34377  erngfmul-rN  34380  dvasca  34573  dvavbase  34580  dvafvadd  34581  dvafvsca  34583  tendocnv  34589  dvhsca  34650  dvhfplusr  34652  dvhvbase  34655  dvhfvadd  34659  dvhfvsca  34668  lcdvadd  35165  lcdsbase  35168  lcdsadd  35169  lcdvs  35171  lcd0  35176  lcd1  35177  lcdneg  35178  imaiinfv  35535  mapfzcons1  35559  rexrabdioph  35637  dnnumch1  35902  dnwech  35906  aomclem6  35917  pwssplit4  35947  pwfi2f1o  35954  mendplusgfval  36051  mendvscafval  36056  uzmptshftfval  36695  dropab1  36800  dropab2  36801  csbunigOLD  37212  csbfv12gALTOLD  37213  csbxpgOLD  37214  csbresgOLD  37216  csbrngOLD  37217  csbima12gALTOLD  37218  itgsinexplem1  37830  wallispi2lem2  37934  fourierdlem36  38006  etransclem4  38103  afveq12d  38635  aoveq123d  38680  aovfundmoveq  38683  aovnuoveq  38693  aovvoveq  38694  aovovn0oveq  38696  resisresindm  39011  fsumsplitsndif  39092  uhgrvtxedgiedgb  39227  nb3grprlem1  39454  rngccofvalALTV  40042  ringccofvalALTV  40105  rhmsubclem2  40142  rhmsubcALTVlem2  40161  xpprsng  40166  aacllem  40593