Theorem 3eqtr4g 2520

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

Syntax hints:   -> wi 4   = wceq 1370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-cleq 2446

This theorem is referenced by:  rabbidva2  3068  rabeqf  3071  csbeq1  3401  difeq1  3578  difeq2  3579  uneq2  3615  ineq2  3657  dfrab3ss  3739  csbeq2d  3797  csbnestgf  3803  ifeq1  3906  ifeq2  3907  pweq  3974  sneq  3998  csbsng  4046  rabsn  4053  preq1  4065  preq2  4066  tpeq1  4074  tpeq2  4075  tpeq3  4076  prprc1  4096  opeq1  4170  opeq2  4171  oteq1  4179  oteq2  4180  oteq3  4181  unieq  4210  csbuni  4230  csbunigOLD  4231  inteq  4242  iineq1  4296  iineq2  4299  dfiin2g  4314  iinrab  4343  iinin1  4352  iinxprg  4359  iununi  4366  opabbid  4465  mpteq12f  4479  csbmpt12  4733  suceq  4895  xpeq1  4965  xpeq2  4966  csbxpgOLD  5030  rneq  5176  reseq1  5215  reseq2  5216  csbresgOLD  5225  resmpt  5267  imaeq1  5275  imaeq2  5276  mptcnv  5350  csbrngOLD  5411  dmpropg  5423  rnpropg  5430  cores  5452  cores2  5461  xpco  5488  iotaeq  5500  iotabi  5501  fntpg  5584  imain  5605  f1oprswap  5791  fveq1  5801  fveq2  5802  fvres  5816  csbfv12  5837  csbfv12gOLD  5838  fnimapr  5867  fvco2  5878  residpr  5998  fsnunfv  6030  fsnunres  6031  funiunfv  6077  fliftf  6120  isoini2  6142  riotaeqdv  6165  riotabidv  6166  riotauni  6170  riotabidva  6181  snriota  6194  oveq  6209  oveq1  6210  oveq2  6211  oprabbid  6251  mpt2eq123  6257  mpt2eq123dva  6259  mpt2eq3dva  6262  resmpt2  6301  ovres  6343  f1ocnvd  6422  ofeq  6435  ofreq  6436  fpar  6789  extmptsuppeq  6826  onovuni  6916  recseq  6946  tfr2a  6967  rdgeq1  6980  rdgeq2  6981  rdgsucmptf  6997  frsucmpt  7006  seqomeq12  7022  seqomsuc  7025  omopthi  7209  eceq1  7250  eceq2  7251  qseq1  7263  qseq2  7264  uniqs  7273  ecinxp  7288  qsinxp  7289  erovlem  7309  ecopovtrn  7316  ixpeq1  7387  supeq1  7809  supeq2  7812  supeq3  7813  supeq123d  7814  oieq1  7840  oieq2  7841  ordtypelem1  7846  inf3lemc  7946  wemapwe  8042  wemapweOLD  8043  r1sucg  8090  r1limg  8092  rankprb  8172  karden  8216  cardiun  8266  acneq  8327  alephlim  8351  alephsuc  8352  alephfplem2  8389  dfac2a  8413  infpssrlem2  8587  fin23lem34  8629  fin23lem35  8630  zorn2lem1  8779  zorn2lem7  8785  fpwwe2lem6  8916  fpwwe2lem13  8923  addpiord  9167  mulpiord  9168  addpqnq  9221  mulpqnq  9224  addassnq  9241  mulassnq  9242  distrnq  9244  lterpq  9253  ltexnq  9258  ltsrpr  9358  00sr  9380  recexsrlem  9384  mulgt0sr  9386  addcnsrec  9424  mulcnsrec  9425  negeq  9716  csbnegg  9721  negsubdi  9779  mulneg1  9895  deceq1  10872  deceq2  10873  xnegeq  11291  fseq1p1m1  11654  om2uzrdg  11899  uzrdgsuci  11903  seqeq1  11929  seqeq2  11930  seqeq3  11931  seqfeq4  11975  seqof  11983  hashprg  12276  hashtpg  12307  hashmap  12318  hashbclem  12326  csbwrdg  12378  s1eq  12412  cats1co  12604  s2eqd  12610  s3eqd  12611  s4eqd  12612  s5eqd  12613  s6eqd  12614  s7eqd  12615  s8eqd  12616  shftval  12684  limsupgle  13076  lo1eq  13167  rlimeq  13168  sumeq1  13287  sumeq2w  13290  sumeq2ii  13291  zsum  13316  sumss2  13324  isumclim3  13347  fsumcom2  13362  fsumrev  13367  incexclem  13420  incexc2  13422  isumshft  13423  ef0lem  13485  ruclem7  13639  sadcp1  13772  smupp1  13797  smueqlem  13807  algrp1  13870  dfphi2  13970  prmdiveq  13982  pceulem  14033  vdwlem6  14168  cshwsiun  14247  setsid  14336  elbasfv  14342  elbasov  14343  imastset  14582  imasvscaval  14598  xpscg  14618  isoval  14825  funcoppc  14907  fulloppc  14954  fuccofval  14991  natpropd  15008  catccofval  15090  xpchomfval  15111  xpccofval  15114  lubfval  15270  glbfval  15283  grpidpropd  15569  gsumpropd2lem  15627  frmdplusg  15654  grpinvpropd  15723  grpsubpropd  15748  grpsubpropd2  15749  mulgpropd  15782  oppgmnd  15991  symgplusg  16016  sylow1lem2  16222  sylow3lem1  16250  prds1  16832  pwsmgp  16836  opprrng  16849  rngidpropd  16913  dvdsrpropd  16914  unitpropd  16915  invrpropd  16916  rhm1  16946  lmhmpropd  17280  lidlrsppropd  17438  lpival  17453  rrgsuppOLD  17489  ressascl  17540  asclpropd  17542  aspval2  17543  psrbas  17574  psrbasOLD  17575  psrplusg  17578  psrmulr  17581  psrvscafval  17587  resspsrbas  17614  ressmplbas2  17661  opsrle  17684  opsrbaslem  17686  mplrcl  17698  vr1val  17775  ressply1add  17811  ressply1mul  17812  ressply1vsca  17813  psrplusgpropd  17817  mplbaspropd  17818  psropprmul  17819  ply1baspropd  17824  ply1plusgpropd  17825  ply1sca2  17835  subrgvr1  17841  coe1mul2lem2  17848  zrhpropd  18074  znle  18095  frlmplusgval  18319  frlmvscafval  18321  mamudi  18435  mamudir  18436  matrcl  18440  oftpos  18463  mattpos1  18470  mdetfval  18527  mdetrlin  18543  mdetrsca  18544  mdetrsca2  18545  mdetrlin2  18548  mdetunilem5  18557  madufval  18578  madugsum  18584  cncmp  19130  2ndcsep  19198  llyeq  19209  nllyeq  19210  xkouni  19307  hmphindis  19505  pt1hmeo  19514  xkocnv  19522  ptcmplem2  19760  snclseqg  19821  prdstmdd  19829  ustexsym  19925  ucnextcn  20014  metreslem  20072  comet  20223  nrmmetd  20302  nmpropd  20321  isngp3  20325  ngpds  20330  subgnm  20354  tngnm  20372  idnghm  20457  cnmetdval  20485  cnmpt2pc  20635  htpyco2  20686  phtpyco2  20697  clsocv  20897  ovolunlem1a  21114  voliunlem3  21169  ioombl1lem4  21178  uniioombllem4  21202  itg11  21305  itgeq1f  21385  itgeq2  21391  iblss2  21419  itgss  21425  itgeqa  21427  itgfsum  21440  itgsplit  21449  ditgeq1  21459  ditgeq2  21460  ditgeq3  21461  dvcmulf  21555  dvmptfsum  21583  dvcnvrelem2  21626  mdegfval  21667  mdegpropd  21691  deg1propd  21693  plyeq0  21815  coe11  21856  dgrlt  21869  dgradd2  21871  dgrmulc  21874  dvply1  21886  fta1lem  21909  pserulm  22023  rlimcnp2  22496  jensenlem1  22516  basellem5  22558  dchrbas  22710  dchrrcl  22715  dchrplusg  22722  dchrfi  22730  lgsdi  22807  lgseisenlem2  22825  lgsquadlem3  22831  dchrmusumlema  22878  rpvmasum2  22897  dchrisum0lema  22899  pntlemg  22983  colperpexlem2  23260  axlowdimlem13  23372  isusgra0  23447  nbgraf1olem5  23526  nb3graprlem1  23531  constr2spthlem1  23665  constr3pthlem1  23713  constr3pthlem2  23714  avril1  23828  0vfval  24156  imsval  24248  imsdval  24249  bcseqi  24694  normpythi  24716  cm0  25184  fh1  25193  pjcji  25259  opsqrlem5  25720  pjsdi2i  25733  pjclem3  25773  pjci  25776  golem1  25847  iunrdx  26085  ofresid  26131  resmptf  26145  f1od2  26195  rhmopp  26452  resv1r  26470  xrge0mulc1cn  26536  qqhval2  26576  esumeq12dvaf  26652  esumeq2  26657  esumf1o  26669  esumfzf  26683  esumss  26686  esumpfinvalf  26690  ofceq  26704  itgeq12dv  26876  ccatmulgnn0dir  27104  cvmliftlem5  27342  cvmliftlem10  27347  cvmlift2lem9  27364  cvmliftphtlem  27370  prodeq1f  27585  prodeq2w  27589  prodeq2ii  27590  zprod  27614  fprodm1s  27644  fprodp1s  27645  fprodshft  27651  fprodrev  27652  fprodcom2  27659  iprodclim3  27664  mpteq12d  27747  rdgprc  27772  dfrdg2  27773  predeq123  27790  trpredeq1  27848  trpredeq2  27849  trpredeq3  27850  wrecseq123  27882  wsuceq123  27915  wlimeq12  27920  symdifeq1  28015  symdifeq2  28016  altopthsn  28156  altxpeq1  28168  altxpeq2  28169  ee7.2aOLD  28471  finixpnum  28582  ptrest  28593  mbfposadd  28607  cnambfre  28608  iblabsnclem  28623  ftc1anclem1  28635  heiborlem4  28881  heiborlem6  28883  mpt2bi123f  29143  iineq12f  29145  mptbi12f  29147  imaiinfv  29197  mapfzcons1  29221  rexrabdioph  29300  dnnumch1  29565  dnwech  29569  aomclem6  29580  pwssplit4  29610  pwfi2f1o  29619  mendplusgfval  29710  mendvscafval  29715  dropab1  29871  dropab2  29872  itgsinexplem1  29962  wallispi2lem2  30035  afveq12d  30207  aoveq123d  30252  aovfundmoveq  30255  aovnuoveq  30265  aovvoveq  30266  aovovn0oveq  30268  csbprg  30285  resisresindm  30307  fsumsplitsndif  30406  fsumsplitsnun  30410  wwlkextwrd  30528  rusgranumwlkl1  30727  rusgranumwlklem3  30737  numclwwlkovf2  30845  xpprsng  30887  ply1coe1eq  31009  idmatidpmat  31246  cpmidpmat  31379  csbfv12gALTOLD  31909  csbima12gALTOLD  31910  bnj956  32122  bnj1385  32178  bnj96  32210  bnj548  32242  bnj553  32243  bnj554  32244  bnj602  32260  bnj18eq1  32272  bnj1234  32356  bnj1296  32364  bnj1318  32368  bnj1442  32392  bnj1450  32393  bj-rabbida2  32772  bj-sngleq  32812  bj-tageq  32821  bj-projeq  32837  bj-projval  32841  bj-1upleq  32844  bj-pr1eq  32847  bj-pr2eq  32861  riotaclbgBAD  32963  riotaclbBAD  32964  toycom  32976  ldualvbase  33129  ldualfvadd  33131  ldualsca  33135  ldualsbase  33136  ldualsaddN  33137  ldualfvs  33139  ldual0  33150  ldual1  33151  ldualneg  33152  cdleme19f  34310  cdleme20m  34325  cdleme21k  34340  cdleme27b  34370  cdleme31so  34381  cdleme31sn  34382  cdleme31se  34384  cdleme31se2  34385  cdleme31sc  34386  cdleme31sde  34387  cdleme31fv  34392  cdleme40v  34471  cdleme43dN  34494  cdlemeg46ngfr  34520  ltrnco4  34741  tgrpbase  34748  tgrpopr  34749  erngbase  34803  erngfplus  34804  erngfmul  34807  erngbase-rN  34811  erngfplus-rN  34812  erngfmul-rN  34815  dvasca  35008  dvavbase  35015  dvafvadd  35016  dvafvsca  35018  tendocnv  35024  dvhsca  35085  dvhfplusr  35087  dvhvbase  35090  dvhfvadd  35094  dvhfvsca  35103  lcdvadd  35600  lcdsbase  35603  lcdsadd  35604  lcdvs  35606  lcd0  35611  lcd1  35612  lcdneg  35613  mapdvalc  35632  mapdval4N  35635