Theorem 3eqtr4g 2489

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 2476	. 2 |- ( ph -> C = B )
4		3eqtr4g.3	. 2 |- D = B
5	3, 4	syl6eqr 2482	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-ext 2401

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

This theorem is referenced by:  rabbidva2  3071  rabeqf  3074  csbeq1  3399  csbeq2  3400  difeq1  3577  difeq2  3578  uneq2  3615  ineq2  3659  symdifeq1  3696  symdifeq2  3697  dfrab3ss  3752  csbeq2d  3809  csbnestgf  3814  ifeq1  3914  ifeq2  3915  pweq  3983  sneq  4007  csbsng  4056  csbprg  4057  rabsn  4065  preq1  4077  preq2  4078  tpeq1  4086  tpeq2  4087  tpeq3  4088  prprc1  4108  opeq1  4185  opeq2  4186  oteq1  4194  oteq2  4195  oteq3  4196  unieq  4225  csbuni  4245  inteq  4256  iineq1  4312  iineq2  4315  dfiin2g  4330  iinrab  4359  iinin1  4368  iinxprg  4378  iununi  4385  opabbid  4484  mpteq12f  4498  csbmpt12  4752  xpeq1  4865  xpeq2  4866  rneq  5077  reseq1  5116  reseq2  5117  resmpt  5171  imaeq1  5180  imaeq2  5181  mptcnv  5255  dmpropg  5326  rnpropg  5333  cores  5355  cores2  5365  xpco  5393  predeq123  5398  suceq  5505  iotaeq  5571  iotabi  5572  fntpg  5654  imain  5675  f1oprswap  5868  fveq1  5878  fveq2  5879  fvres  5893  csbfv12  5914  fnimapr  5943  fvco2  5954  residpr  6081  fsnunfv  6117  fsnunres  6118  funiunfv  6166  fliftf  6221  isoini2  6243  riotaeqdv  6266  riotabidv  6267  riotauni  6271  riotabidva  6281  snriota  6294  oveq  6309  oveq1  6310  oveq2  6311  oprabbid  6356  mpt2eq123  6362  mpt2eq123dva  6364  mpt2eq3dva  6367  resmpt2  6406  ovres  6448  f1ocnvd  6530  ofeq  6545  ofreq  6546  fpar  6909  wrecseq123  7035  onovuni  7067  recseq  7098  tfr2a  7119  rdgeq1  7135  rdgeq2  7136  rdgsucmptf  7152  frsucmpt  7161  seqomeq12  7177  seqomsuc  7180  omopthi  7364  eceq1  7405  eceq2  7407  qseq1  7419  qseq2  7420  uniqs  7429  ecinxp  7444  qsinxp  7445  erovlem  7465  ecopovtrn  7472  ixpeq1  7539  supeq1  7963  supeq2  7966  supeq3  7967  supeq123d  7968  infeq1  7996  infeq2  7999  infeq3  8000  infeq123d  8001  infiso  8027  oieq1  8031  oieq2  8032  ordtypelem1  8037  inf3lemc  8135  wemapwe  8205  r1sucg  8243  r1limg  8245  rankprb  8325  karden  8369  cardiun  8419  acneq  8476  alephlim  8500  alephsuc  8501  alephfplem2  8538  infpssrlem2  8736  fin23lem34  8778  fin23lem35  8779  zorn2lem1  8928  zorn2lem7  8934  fpwwe2lem6  9062  fpwwe2lem13  9069  addpiord  9311  mulpiord  9312  addpqnq  9365  mulpqnq  9368  addassnq  9385  mulassnq  9386  distrnq  9388  lterpq  9397  ltexnq  9402  ltsrpr  9503  00sr  9525  recexsrlem  9529  mulgt0sr  9531  addcnsrec  9569  mulcnsrec  9570  negeq  9869  csbnegg  9874  negsubdi  9932  mulneg1  10057  negfi  10556  deceq1  11056  deceq2  11057  xnegeq  11502  fseq1p1m1  11870  om2uzrdg  12171  uzrdgsuci  12175  seqeq1  12217  seqeq2  12218  seqeq3  12219  seqfeq4  12263  seqof  12271  hashprg  12573  hashmap  12606  hashtpg  12639  csbwrdg  12694  s1eq  12737  cats1co  12948  s2eqd  12954  s3eqd  12955  s4eqd  12956  s5eqd  12957  s6eqd  12958  s7eqd  12959  s8eqd  12960  xpcogend  13032  shftval  13131  limsupgle  13528  lo1eq  13625  rlimeq  13626  sumeq1  13748  sumeq2w  13751  sumeq2ii  13752  zsum  13777  sumss2  13785  fsumsplitsnun  13809  isumclim3  13813  fsumcom2  13828  incexclem  13887  incexc2  13889  isumshft  13890  prodeq1f  13955  prodeq2w  13959  prodeq2ii  13960  zprod  13984  fprodm1s  14017  fprodp1s  14018  fprodcom2  14031  iprodclim3  14046  ef0lem  14126  ruclem7  14281  sadcp1  14422  smupp1  14447  smueqlem  14457  algrp1  14526  dfphi2  14715  prmdiveq  14727  pceulem  14788  vdwlem6  14929  cshwsiun  15063  setsid  15157  elbasfv  15163  elbasov  15164  imastset  15416  imasvscaval  15437  xpscg  15457  isoval  15663  funcoppc  15773  fulloppc  15820  fuccofval  15857  natpropd  15874  catccofval  15988  xpchomfval  16057  xpccofval  16060  lubfval  16217  glbfval  16230  grpidpropd  16497  gsumpropd2lem  16509  frmdplusg  16631  grpinvpropd  16722  grpsubpropd  16749  grpsubpropd2  16750  mulgpropd  16784  oppgmnd  16998  symgplusg  17023  sylow1lem2  17244  sylow3lem1  17272  prds1  17835  pwsmgp  17839  opprring  17852  rngidpropd  17916  dvdsrpropd  17917  unitpropd  17918  invrpropd  17919  rhm1  17951  lmhmpropd  18289  lidlrsppropd  18447  lpival  18462  ressascl  18561  asclpropd  18563  aspval2  18564  psrbas  18595  psrplusg  18598  psrmulr  18601  psrvscafval  18607  resspsrbas  18632  ressmplbas2  18672  opsrle  18692  opsrbaslem  18694  vr1val  18778  ressply1add  18816  ressply1mul  18817  ressply1vsca  18818  psrplusgpropd  18822  mplbaspropd  18823  psropprmul  18824  ply1baspropd  18829  ply1plusgpropd  18830  ply1sca2  18840  subrgvr1  18847  coe1mul2lem2  18854  ply1coe1eq  18885  zrhpropd  19078  znle  19099  frlmplusgval  19318  frlmvscafval  19320  mamudi  19420  mamudir  19421  matrcl  19429  oftpos  19469  mattpos1  19473  mdetfval  19603  mdetrlin  19619  mdetrsca  19620  mdetrsca2  19621  mdetrlin2  19624  mdetunilem5  19633  madufval  19654  madugsum  19660  idmatidpmat  19753  cpmidpmat  19889  cncmp  20399  2ndcsep  20466  llyeq  20477  nllyeq  20478  xkouni  20606  hmphindis  20804  xkocnv  20821  ptcmplem2  21060  snclseqg  21122  prdstmdd  21130  ustexsym  21222  ucnextcn  21311  metreslem  21369  comet  21520  nrmmetd  21581  nmpropd  21600  isngp3  21604  ngpds  21609  subgnm  21633  tngnm  21651  idnghm  21756  cnmetdval  21783  cnmpt2pc  21948  htpyco2  22002  phtpyco2  22013  clsocv  22213  rrxprds  22340  rrxnm  22342  ovolunlem1a  22441  voliunlem3  22497  ioombl1lem4  22506  uniioombllem4  22536  itg11  22641  itgeq1f  22721  itgeq2  22727  iblss2  22755  itgss  22761  itgeqa  22763  itgfsum  22776  itgsplit  22785  ditgeq1  22795  ditgeq2  22796  ditgeq3  22797  dvcmulf  22891  dvmptfsum  22919  dvcnvrelem2  22962  mdegfval  23003  mdegpropd  23025  deg1propd  23027  plyeq0  23157  coe11  23199  dgrlt  23212  dgradd2  23214  dgrmulc  23217  dvply1  23229  fta1lem  23252  pserulm  23369  rlimcnp2  23884  jensenlem1  23904  basellem5  24003  dchrbas  24155  dchrrcl  24160  dchrplusg  24167  dchrfi  24175  lgsdi  24252  lgseisenlem2  24270  lgsquadlem3  24276  dchrmusumlema  24323  rpvmasum2  24342  dchrisum0lema  24344  pntlemg  24428  colperpexlem2  24765  axlowdimlem13  24976  nbgraf1olem5  25165  nb3graprlem1  25171  constr2spthlem1  25316  constr3pthlem1  25375  constr3pthlem2  25376  avril1  25892  0vfval  26217  imsval  26309  imsdval  26310  bcseqi  26765  normpythi  26787  cm0  27254  fh1  27263  pjcji  27329  opsqrlem5  27789  pjsdi2i  27802  pjclem3  27842  pjci  27845  golem1  27916  iunrdx  28175  ofresid  28239  mpteq12df  28252  resmptf  28253  f1od2  28309  gsumvsca1  28547  gsumvsca2  28548  rhmopp  28584  resv1r  28602  fzto1st1  28617  crefeq  28674  xrge0mulc1cn  28749  qqhval2  28788  esumeq12dvaf  28854  esumeq2  28859  esumf1o  28873  esumfzf  28892  esumss  28895  esumpfinvalf  28899  ofceq  28920  itgeq12dv  29161  ccatmulgnn0dir  29430  bnj956  29590  bnj1385  29646  bnj96  29678  bnj548  29710  bnj553  29711  bnj554  29712  bnj602  29728  bnj18eq1  29740  bnj1234  29824  bnj1296  29832  bnj1318  29836  bnj1442  29860  bnj1450  29861  cvmliftlem5  30014  cvmliftlem10  30019  cvmlift2lem9  30036  cvmliftphtlem  30042  mthmpps  30222  mpteq12d  30413  rdgprc  30442  dfrdg2  30443  trpredeq1  30462  trpredeq2  30463  trpredeq3  30464  wsuceq123  30498  wlimeq12  30503  altopthsn  30727  altxpeq1  30739  altxpeq2  30740  ee7.2aOLD  31120  bj-rabbida2  31483  bj-sngleq  31523  bj-tageq  31532  bj-projeq  31548  bj-projval  31552  bj-1upleq  31555  bj-pr1eq  31558  bj-pr2eq  31572  csbopg2  31683  csbpredg  31685  csbwrecsg  31686  csbrecsg  31687  csbrdgg  31688  csboprabg  31689  csbmpt22g  31690  finxpeq1  31736  finxpeq2  31737  csbfinxpg  31738  finxpreclem4  31744  finixpnum  31888  ptrest  31897  poimirlem3  31901  poimirlem9  31907  poimirlem15  31913  poimirlem16  31914  poimirlem26  31924  poimirlem27  31925  mbfposadd  31946  cnambfre  31947  iblabsnclem  31963  ftc1anclem1  31975  heiborlem4  32104  heiborlem6  32106  mpt2bi123f  32364  iineq12f  32366  mptbi12f  32368  riotaclbgBAD  32489  toycom  32502  ldualvbase  32655  ldualfvadd  32657  ldualsca  32661  ldualsbase  32662  ldualsaddN  32663  ldualfvs  32665  ldual0  32676  ldual1  32677  ldualneg  32678  cdleme19f  33838  cdleme20m  33853  cdleme21k  33868  cdleme27b  33898  cdleme31so  33909  cdleme31sn  33910  cdleme31se  33912  cdleme31se2  33913  cdleme31sc  33914  cdleme31sde  33915  cdleme31fv  33920  cdleme40v  33999  cdleme43dN  34022  cdlemeg46ngfr  34048  ltrnco4  34269  tgrpbase  34276  tgrpopr  34277  erngbase  34331  erngfplus  34332  erngfmul  34335  erngbase-rN  34339  erngfplus-rN  34340  erngfmul-rN  34343  dvasca  34536  dvavbase  34543  dvafvadd  34544  dvafvsca  34546  tendocnv  34552  dvhsca  34613  dvhfplusr  34615  dvhvbase  34618  dvhfvadd  34622  dvhfvsca  34631  lcdvadd  35128  lcdsbase  35131  lcdsadd  35132  lcdvs  35134  lcd0  35139  lcd1  35140  lcdneg  35141  imaiinfv  35498  mapfzcons1  35522  rexrabdioph  35600  dnnumch1  35866  dnwech  35870  aomclem6  35881  pwssplit4  35911  pwfi2f1o  35918  mendplusgfval  36015  mendvscafval  36020  uzmptshftfval  36597  dropab1  36702  dropab2  36703  csbunigOLD  37117  csbfv12gALTOLD  37118  csbxpgOLD  37119  csbresgOLD  37121  csbrngOLD  37122  csbima12gALTOLD  37123  itgsinexplem1  37694  wallispi2lem2  37798  fourierdlem36  37870  etransclem4  37967  afveq12d  38391  aoveq123d  38436  aovfundmoveq  38439  aovnuoveq  38449  aovvoveq  38450  aovovn0oveq  38452  resisresindm  38755  fsumsplitsndif  38800  rngccofvalALTV  39331  ringccofvalALTV  39394  rhmsubclem2  39431  rhmsubcALTVlem2  39450  xpprsng  39457  aacllem  39884