Theorem 3eqtr4g 2490

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-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 2477	. 2 |- ( ph -> C = B )
4		3eqtr4g.3	. 2 |- D = B
5	3, 4	syl6eqr 2483	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-ex 1590  df-cleq 2426

This theorem is referenced by:  rabbidva2  2952  rabeqf  2955  csbeq1  3279  difeq1  3455  difeq2  3456  uneq2  3492  ineq2  3534  dfrab3ss  3616  csbeq2d  3674  csbnestgf  3680  ifeq1  3783  ifeq2  3784  pweq  3851  sneq  3875  csbsng  3923  rabsn  3930  preq1  3942  preq2  3943  tpeq1  3951  tpeq2  3952  tpeq3  3953  prprc1  3973  opeq1  4047  opeq2  4048  oteq1  4056  oteq2  4057  oteq3  4058  unieq  4087  csbuni  4107  csbunigOLD  4108  inteq  4119  iineq1  4173  iineq2  4176  dfiin2g  4191  iinrab  4220  iinin1  4229  iinxprg  4236  iununi  4243  opabbid  4342  mpteq12f  4356  suceq  4771  xpeq1  4841  xpeq2  4842  csbxpgOLD  4906  rneq  5052  reseq1  5091  reseq2  5092  csbresgOLD  5101  resmpt  5144  imaeq1  5152  imaeq2  5153  mptcnv  5227  csbrngOLD  5288  dmpropg  5300  rnpropg  5307  cores  5329  cores2  5338  xpco  5365  iotaeq  5377  iotabi  5378  fntpg  5461  imain  5482  f1oprswap  5668  fveq1  5678  fveq2  5679  fvres  5692  csbfv12  5713  csbfv12gOLD  5714  fnimapr  5743  fvco2  5754  residpr  5873  fsnunfv  5905  fsnunres  5906  funiunfv  5952  fliftf  5995  isoini2  6017  riotaeqdv  6040  riotabidv  6041  riotauni  6046  riotabidva  6057  snriota  6070  oveq  6086  oveq1  6087  oveq2  6088  oprabbid  6128  mpt2eq123  6134  mpt2eq123dva  6136  mpt2eq3dva  6139  resmpt2  6177  ovres  6219  f1ocnvd  6298  ofeq  6311  ofreq  6312  fpar  6665  extmptsuppeq  6702  onovuni  6789  recseq  6819  tfr2a  6840  rdgeq1  6853  rdgeq2  6854  rdgsucmptf  6870  frsucmpt  6879  seqomeq12  6895  seqomsuc  6898  abianfplem  6899  omopthi  7084  eceq1  7125  eceq2  7126  qseq1  7138  qseq2  7139  uniqs  7148  ecinxp  7163  qsinxp  7164  erovlem  7184  ecopovtrn  7191  ixpeq1  7262  supeq1  7683  supeq2  7686  supeq3  7687  supeq123d  7688  oieq1  7714  oieq2  7715  ordtypelem1  7720  inf3lemc  7820  wemapwe  7916  wemapweOLD  7917  r1sucg  7964  r1limg  7966  rankprb  8046  karden  8090  cardiun  8140  acneq  8201  alephlim  8225  alephsuc  8226  alephfplem2  8263  dfac2a  8287  infpssrlem2  8461  fin23lem34  8503  fin23lem35  8504  zorn2lem1  8653  zorn2lem7  8659  fpwwe2lem6  8789  fpwwe2lem13  8796  addpiord  9040  mulpiord  9041  addpqnq  9094  mulpqnq  9097  addassnq  9114  mulassnq  9115  distrnq  9117  lterpq  9126  ltexnq  9131  ltsrpr  9231  00sr  9253  recexsrlem  9257  mulgt0sr  9259  addcnsrec  9297  mulcnsrec  9298  negeq  9589  csbnegg  9594  negsubdi  9652  mulneg1  9768  deceq1  10745  deceq2  10746  xnegeq  11164  fseq1p1m1  11517  om2uzrdg  11762  uzrdgsuci  11766  seqeq1  11792  seqeq2  11793  seqeq3  11794  seqfeq4  11838  seqof  11846  hashprg  12138  hashtpg  12169  hashmap  12180  hashbclem  12188  csbwrdg  12240  s1eq  12274  cats1co  12466  s2eqd  12472  s3eqd  12473  s4eqd  12474  s5eqd  12475  s6eqd  12476  s7eqd  12477  s8eqd  12478  shftval  12546  limsupgle  12938  lo1eq  13029  rlimeq  13030  sumeq1  13149  sumeq2w  13152  sumeq2ii  13153  zsum  13178  sumss2  13186  isumclim3  13209  fsumcom2  13224  fsumrev  13228  fsumshft  13229  incexclem  13281  incexc2  13283  isumshft  13284  ef0lem  13346  ruclem7  13500  sadcp1  13633  smupp1  13658  smueqlem  13668  algrp1  13731  dfphi2  13831  prmdiveq  13843  pceulem  13894  vdwlem6  14029  cshwsiun  14108  setsid  14197  elbasfv  14203  elbasov  14204  imastset  14442  imasvscaval  14458  xpscg  14478  isoval  14685  funcoppc  14767  fulloppc  14814  fuccofval  14851  natpropd  14868  catccofval  14950  xpchomfval  14971  xpccofval  14974  lubfval  15130  glbfval  15143  grpidpropd  15429  frmdplusg  15511  grpinvpropd  15580  grpsubpropd  15605  grpsubpropd2  15606  mulgpropd  15639  oppgmnd  15848  symgplusg  15873  sylow1lem2  16077  sylow3lem1  16105  prds1  16640  pwsmgp  16644  opprrng  16656  rngidpropd  16720  dvdsrpropd  16721  unitpropd  16722  invrpropd  16723  rhm1  16751  lmhmpropd  17075  lidlrsppropd  17233  lpival  17248  rrgsuppOLD  17284  ressascl  17335  asclpropd  17337  aspval2  17338  psrbas  17381  psrbasOLD  17382  psrplusg  17385  psrmulr  17388  psrvscafval  17394  resspsrbas  17420  ressmplbas2  17467  opsrle  17488  opsrbaslem  17490  mplrcl  17502  vr1val  17546  ressply1add  17582  ressply1mul  17583  ressply1vsca  17584  psrplusgpropd  17587  mplbaspropd  17588  strov2rcl  17589  psropprmul  17590  ply1baspropd  17595  ply1plusgpropd  17596  ply1sca2  17606  subrgvr1  17612  coe1mul2lem2  17619  zrhpropd  17787  znle  17808  frlmplusgval  18032  frlmvscafval  18034  mamudi  18148  mamudir  18149  matrcl  18153  oftpos  18174  mattpos1  18181  mdetfval  18238  mdetrlin  18250  mdetrsca  18251  mdetrsca2  18252  mdetrlin2  18254  mdetunilem5  18263  madufval  18284  madugsum  18290  cncmp  18836  2ndcsep  18904  llyeq  18915  nllyeq  18916  xkouni  19013  hmphindis  19211  pt1hmeo  19220  xkocnv  19228  ptcmplem2  19466  snclseqg  19527  prdstmdd  19535  ustexsym  19631  ucnextcn  19720  metreslem  19778  comet  19929  nrmmetd  20008  nmpropd  20027  isngp3  20031  ngpds  20036  subgnm  20060  tngnm  20078  idnghm  20163  cnmetdval  20191  cnmpt2pc  20341  htpyco2  20392  phtpyco2  20403  clsocv  20603  ovolunlem1a  20820  voliunlem3  20874  ioombl1lem4  20883  uniioombllem4  20907  itg11  21010  itgeq1f  21090  itgeq2  21096  iblss2  21124  itgss  21130  itgeqa  21132  itgfsum  21145  itgsplit  21154  ditgeq1  21164  ditgeq2  21165  ditgeq3  21166  dvcmulf  21260  dvmptfsum  21288  dvcnvrelem2  21331  mdegfval  21415  mdegpropd  21439  deg1propd  21441  plyeq0  21563  coe11  21604  dgrlt  21617  dgradd2  21619  dgrmulc  21622  dvply1  21634  fta1lem  21657  pserulm  21771  rlimcnp2  22244  jensenlem1  22264  basellem5  22306  dchrbas  22458  dchrrcl  22463  dchrplusg  22470  dchrfi  22478  lgsdi  22555  lgseisenlem2  22573  lgsquadlem3  22579  dchrmusumlema  22626  rpvmasum2  22645  dchrisum0lema  22647  pntlemg  22731  axlowdimlem13  23022  isusgra0  23097  nbgraf1olem5  23176  nb3graprlem1  23181  constr2spthlem1  23315  constr3pthlem1  23363  constr3pthlem2  23364  avril1  23478  0vfval  23806  imsval  23898  imsdval  23899  bcseqi  24344  normpythi  24366  cm0  24834  fh1  24843  pjcji  24909  opsqrlem5  25370  pjsdi2i  25383  pjclem3  25423  pjci  25426  golem1  25497  iunrdx  25737  ofresid  25783  resmptf  25797  f1od2  25847  gsumpropd2lem  26092  rhmopp  26139  resv1r  26158  xrge0mulc1cn  26224  qqhval2  26264  esumeq12dvaf  26340  esumeq2  26345  esumf1o  26357  esumfzf  26371  esumss  26374  esumpfinvalf  26378  ofceq  26392  itgeq12dv  26559  ccatmulgnn0dir  26787  cvmliftlem5  27025  cvmliftlem10  27030  cvmlift2lem9  27047  cvmliftphtlem  27053  prodeq1f  27267  prodeq2w  27271  prodeq2ii  27272  zprod  27296  fprodm1s  27326  fprodp1s  27327  fprodshft  27333  fprodrev  27334  fprodcom2  27341  iprodclim3  27346  mpteq12d  27429  rdgprc  27454  dfrdg2  27455  predeq123  27472  trpredeq1  27530  trpredeq2  27531  trpredeq3  27532  wrecseq123  27564  wsuceq123  27597  wlimeq12  27602  symdifeq1  27697  symdifeq2  27698  altopthsn  27838  altxpeq1  27850  altxpeq2  27851  ee7.2aOLD  28154  finixpnum  28255  ptrest  28266  mbfposadd  28280  cnambfre  28281  iblabsnclem  28296  ftc1anclem1  28308  heiborlem4  28554  heiborlem6  28556  iineq12f  28818  imaiinfv  28871  mapfzcons1  28895  rexrabdioph  28974  dnnumch1  29239  dnwech  29243  aomclem6  29254  pwssplit4  29284  pwfi2f1o  29293  mendplusgfval  29384  mendvscafval  29389  dropab1  29545  dropab2  29546  itgsinexplem1  29637  wallispi2lem2  29710  afveq12d  29882  aoveq123d  29927  aovfundmoveq  29930  aovnuoveq  29940  aovvoveq  29941  aovovn0oveq  29943  csbprg  29960  resisresindm  29982  fsumsplitsndif  30081  fsumsplitsnun  30085  wwlkextwrd  30203  rusgranumwlkl1  30402  rusgranumwlklem3  30412  numclwwlkovf2  30520  xpprsng  30561  csbfv12gALTOLD  31256  csbima12gALTOLD  31257  bnj956  31469  bnj1385  31525  bnj96  31557  bnj548  31589  bnj553  31590  bnj554  31591  bnj602  31607  bnj18eq1  31619  bnj1234  31703  bnj1296  31711  bnj1318  31715  bnj1442  31739  bnj1450  31740  bj-rabbida2  32004  bj-sngleq  32040  bj-tageq  32049  bj-projeq  32065  bj-projval  32069  bj-1upleq  32072  bj-pr1eq  32075  bj-pr2eq  32089  riotaclbgBAD  32175  riotaclbBAD  32176  toycom  32188  ldualvbase  32341  ldualfvadd  32343  ldualsca  32347  ldualsbase  32348  ldualsaddN  32349  ldualfvs  32351  ldual0  32362  ldual1  32363  ldualneg  32364  cdleme19f  33522  cdleme20m  33537  cdleme21k  33552  cdleme27b  33582  cdleme31so  33593  cdleme31sn  33594  cdleme31se  33596  cdleme31se2  33597  cdleme31sc  33598  cdleme31sde  33599  cdleme31fv  33604  cdleme40v  33683  cdleme43dN  33706  cdlemeg46ngfr  33732  ltrnco4  33953  tgrpbase  33960  tgrpopr  33961  erngbase  34015  erngfplus  34016  erngfmul  34019  erngbase-rN  34023  erngfplus-rN  34024  erngfmul-rN  34027  dvasca  34220  dvavbase  34227  dvafvadd  34228  dvafvsca  34230  tendocnv  34236  dvhsca  34297  dvhfplusr  34299  dvhvbase  34302  dvhfvadd  34306  dvhfvsca  34315  lcdvadd  34812  lcdsbase  34815  lcdsadd  34816  lcdvs  34818  lcd0  34823  lcd1  34824  lcdneg  34825  mapdvalc  34844  mapdval4N  34847