Theorem 3eqtr4g 2461

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

Syntax hints:   -> wi 4   = wceq 1649

This theorem is referenced by:  rabeqf  2909  csbeq1  3214  csbeq2d  3235  csbnestgf  3259  difeq1  3418  difeq2  3419  uneq2  3455  ineq2  3496  dfrab3ss  3579  ifeq1  3703  ifeq2  3704  pweq  3762  sneq  3785  csbsng  3827  rabsn  3833  preq1  3843  preq2  3844  tpeq1  3852  tpeq2  3853  tpeq3  3854  prprc1  3874  opeq1  3944  opeq2  3945  oteq1  3953  oteq2  3954  oteq3  3955  csbunig  3983  unieq  3984  inteq  4013  iineq1  4067  iineq2  4070  dfiin2g  4084  iinrab  4113  iinin1  4122  iinxprg  4128  iununi  4135  opabbid  4230  mpteq12f  4245  suceq  4606  xpeq1  4851  xpeq2  4852  csbxpg  4864  rneq  5054  csbrng  5073  reseq1  5099  reseq2  5100  csbresg  5108  resmpt  5150  imaeq1  5157  imaeq2  5158  csbima12gALT  5173  dmpropg  5302  cores  5332  cores2  5341  xpco  5373  iotaeq  5385  iotabi  5386  fntpg  5465  imain  5488  f1oprswap  5676  fveq1  5686  fveq2  5687  csbfv12g  5697  csbfv12gALT  5698  fvres  5704  fnimapr  5746  fvco2  5757  fsnunfv  5892  fsnunres  5893  funiunfv  5954  fliftf  5996  isoini2  6018  oveq  6046  oveq1  6047  oveq2  6048  oprabbid  6086  mpt2eq123  6092  mpt2eq123dva  6094  mpt2eq3dva  6097  resmpt2  6127  ovres  6172  f1ocnvd  6252  ofeq  6266  ofreq  6267  fpar  6409  riotaeqdv  6509  riotabidv  6510  riotabidva  6525  riotaund  6545  onovuni  6563  recseq  6593  tfr2a  6615  rdgeq1  6628  rdgeq2  6629  rdgsucmptf  6645  frsucmpt  6654  seqomeq12  6670  seqomsuc  6673  abianfplem  6674  omopthi  6859  eceq1  6900  eceq2  6901  qseq1  6913  qseq2  6914  uniqs  6923  ecinxp  6938  qsinxp  6939  erovlem  6959  ecopovtrn  6966  ixpeq1  7032  supeq1  7408  supeq2  7411  oieq1  7437  oieq2  7438  ordtypelem1  7443  inf3lemc  7537  cantnfreslem  7587  wemapwe  7610  r1sucg  7651  r1limg  7653  rankprb  7733  karden  7775  cardiun  7825  acneq  7880  alephlim  7904  alephsuc  7905  alephfplem2  7942  dfac2a  7966  infpssrlem2  8140  fin23lem34  8182  fin23lem35  8183  zorn2lem1  8332  zorn2lem7  8338  fpwwe2lem6  8466  fpwwe2lem13  8473  addpiord  8717  mulpiord  8718  addpqnq  8771  mulpqnq  8774  addassnq  8791  mulassnq  8792  distrnq  8794  lterpq  8803  ltexnq  8808  ltsrpr  8908  00sr  8930  recexsrlem  8934  mulgt0sr  8936  addcnsrec  8974  mulcnsrec  8975  negeq  9254  csbnegg  9259  negsubdi  9313  mulneg1  9426  deceq1  10341  deceq2  10342  xnegeq  10749  fseq1p1m1  11077  om2uzrdg  11251  uzrdgsuci  11255  seqeq1  11281  seqeq2  11282  seqeq3  11283  seqfeq4  11327  seqof  11335  hashprg  11621  hashtpg  11646  hashmap  11653  hashbclem  11656  s1eq  11708  cats1co  11775  s2eqd  11781  s3eqd  11782  s4eqd  11783  s5eqd  11784  s6eqd  11785  s7eqd  11786  s8eqd  11787  shftval  11844  limsupgle  12226  lo1eq  12317  rlimeq  12318  sumeq1f  12437  sumeq2w  12441  sumeq2ii  12442  zsum  12467  sumss2  12475  isumclim3  12498  fsumcom2  12513  fsumrev  12517  fsumshft  12518  incexclem  12571  incexc2  12573  isumshft  12574  ef0lem  12636  ruclem7  12790  sadcp1  12922  smupp1  12947  smueqlem  12957  algrp1  13020  dfphi2  13118  prmdiveq  13130  pceulem  13174  vdwlem6  13309  setsid  13463  elbasfv  13467  elbasov  13468  imastset  13702  imasvscaval  13718  xpscg  13738  isoval  13945  funcoppc  14027  fulloppc  14074  fuccofval  14111  natpropd  14128  catccofval  14210  xpchomfval  14231  xpccofval  14234  grpidpropd  14677  frmdplusg  14754  grpinvpropd  14821  grpsubpropd  14844  grpsubpropd2  14845  mulgpropd  14878  symgplusg  15054  oppgmnd  15105  sylow1lem2  15188  sylow3lem1  15216  prds1  15675  pwsmgp  15679  opprrng  15691  rngidpropd  15755  dvdsrpropd  15756  unitpropd  15757  invrpropd  15758  rhm1  15786  lmhmpropd  16100  lidlrsppropd  16256  lpival  16271  rrgsupp  16306  ressascl  16357  asclpropd  16359  aspval2  16360  psrbas  16398  psrplusg  16400  psrmulr  16403  psrvscafval  16409  resspsrbas  16433  ressmplbas2  16473  opsrle  16491  opsrbaslem  16493  mplrcl  16505  vr1val  16545  ressply1add  16579  ressply1mul  16580  ressply1vsca  16581  psrplusgpropd  16584  mplbaspropd  16585  strov2rcl  16586  psropprmul  16587  ply1baspropd  16592  ply1plusgpropd  16593  ply1sca2  16603  subrgvr1  16609  coe1mul2lem2  16616  zrhpropd  16751  znle  16772  cncmp  17409  2ndcsep  17475  llyeq  17486  nllyeq  17487  xkouni  17584  hmphindis  17782  pt1hmeo  17791  xkocnv  17799  ptcmplem2  18037  snclseqg  18098  prdstmdd  18106  ustexsym  18198  ucnextcn  18287  metreslem  18345  comet  18496  nrmmetd  18575  nmpropd  18594  isngp3  18598  ngpds  18603  subgnm  18627  tngnm  18645  idnghm  18730  cnmetdval  18758  cnmpt2pc  18906  htpyco2  18957  phtpyco2  18968  clsocv  19157  ovolunlem1a  19345  voliunlem3  19399  ioombl1lem4  19408  uniioombllem4  19431  itg11  19536  itgeq1f  19616  itgeq2  19622  iblss2  19650  itgss  19656  itgeqa  19658  itgfsum  19671  itgsplit  19680  ditgeq1  19688  ditgeq2  19689  ditgeq3  19690  dvcmulf  19784  dvmptfsum  19812  dvcnvrelem2  19855  mdegfval  19938  mdegpropd  19960  deg1propd  19962  plyeq0  20083  coe11  20124  dgrlt  20137  dgradd2  20139  dgrmulc  20142  dvply1  20154  fta1lem  20177  pserulm  20291  rlimcnp2  20758  jensenlem1  20778  basellem5  20820  dchrbas  20972  dchrrcl  20977  dchrplusg  20984  dchrfi  20992  lgsdi  21069  lgseisenlem2  21087  lgsquadlem3  21093  dchrmusumlema  21140  rpvmasum2  21159  dchrisum0lema  21161  pntlemg  21245  isusgra0  21329  nbgraf1olem5  21408  nb3graprlem1  21413  constr2spthlem1  21547  constr3pthlem1  21595  constr3pthlem2  21596  avril1  21710  0vfval  22038  imsval  22130  imsdval  22131  bcseqi  22575  normpythi  22597  cm0  23064  fh1  23073  pjcji  23139  opsqrlem5  23600  pjsdi2i  23613  pjclem3  23653  pjci  23656  golem1  23727  rabbidva2  23939  iunrdx  23967  rnpropg  23988  mptcnv  23998  ofresid  24008  resmptf  24024  gsumpropd2lem  24173  rhmopp  24210  xrge0mulc1cn  24280  qqhval2  24319  esumeq12dvaf  24381  esumeq2  24386  esumf1o  24398  esumfzf  24412  esumss  24415  esumpfinvalf  24419  ofceq  24433  itgeq12dv  24594  cvmliftlem5  24929  cvmliftlem10  24934  cvmlift2lem9  24951  cvmliftphtlem  24957  prodeq1f  25187  prodeq2w  25191  prodeq2ii  25192  zprod  25216  fprodm1s  25246  fprodp1s  25247  fprodshft  25253  fprodrev  25254  fprodcom2  25261  iprodclim3  25266  mpteq12d  25342  rdgprc  25365  dfrdg2  25366  predeq1  25383  predeq2  25384  predeq3  25385  trpredeq1  25437  trpredeq2  25438  trpredeq3  25439  symdifeq1  25578  symdifeq2  25579  altopthsn  25710  altxpeq1  25722  altxpeq2  25723  axlowdimlem13  25797  ee7.2aOLD  26115  mbfposadd  26153  cnambfre  26154  iblabsnclem  26167  heiborlem4  26413  heiborlem6  26415  imaiinfv  26630  mapfzcons1  26663  rexrabdioph  26744  dnnumch1  27009  dnwech  27013  aomclem6  27024  supeq123d  27026  pwssplit4  27059  frlmplusgval  27097  frlmvscafval  27098  pwfi2f1o  27128  mamudi  27329  mamudir  27330  matrcl  27334  mdetfval  27355  mendplusgfval  27361  mendvscafval  27366  dropab1  27517  dropab2  27518  itgsinexplem1  27615  wallispi2lem2  27688  csbdmg  27849  afveq12d  27864  aoveq123d  27909  aovfundmoveq  27912  aovnuoveq  27922  aovvoveq  27923  aovovn0oveq  27925  resisresindm  27957  bnj956  28853  bnj1385  28910  bnj96  28942  bnj548  28974  bnj553  28975  bnj554  28976  bnj602  28992  bnj18eq1  29004  bnj1234  29088  bnj1296  29096  bnj1318  29100  bnj1442  29124  bnj1450  29125  toycom  29455  ldualvbase  29609  ldualfvadd  29611  ldualsca  29615  ldualsbase  29616  ldualsaddN  29617  ldualfvs  29619  ldual0  29630  ldual1  29631  ldualneg  29632  cdleme19f  30790  cdleme20m  30805  cdleme21k  30820  cdleme27b  30850  cdleme31so  30861  cdleme31sn  30862  cdleme31se  30864  cdleme31se2  30865  cdleme31sc  30866  cdleme31sde  30867  cdleme31fv  30872  cdleme40v  30951  cdleme43dN  30974  cdlemeg46ngfr  31000  ltrnco4  31221  tgrpbase  31228  tgrpopr  31229  erngbase  31283  erngfplus  31284  erngfmul  31287  erngbase-rN  31291  erngfplus-rN  31292  erngfmul-rN  31295  dvasca  31488  dvavbase  31495  dvafvadd  31496  dvafvsca  31498  tendocnv  31504  dvhsca  31565  dvhfplusr  31567  dvhvbase  31570  dvhfvadd  31574  dvhfvsca  31583  lcdvadd  32080  lcdsbase  32083  lcdsadd  32084  lcdvs  32086  lcd0  32091  lcd1  32092  lcdneg  32093  mapdvalc  32112  mapdval4N  32115

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397