Theorem 3eqtr4g 2533

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

Syntax hints:   -> wi 4   = wceq 1379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

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

This theorem is referenced by:  rabbidva2  3103  rabeqf  3106  csbeq1  3438  difeq1  3615  difeq2  3616  uneq2  3652  ineq2  3694  dfrab3ss  3776  csbeq2d  3834  csbnestgf  3840  ifeq1  3943  ifeq2  3944  pweq  4013  sneq  4037  csbsng  4086  csbprg  4087  rabsn  4094  preq1  4106  preq2  4107  tpeq1  4115  tpeq2  4116  tpeq3  4117  prprc1  4137  opeq1  4213  opeq2  4214  oteq1  4222  oteq2  4223  oteq3  4224  unieq  4253  csbuni  4273  csbunigOLD  4274  inteq  4285  iineq1  4340  iineq2  4343  dfiin2g  4358  iinrab  4387  iinin1  4396  iinxprg  4403  iununi  4410  opabbid  4509  mpteq12f  4523  csbmpt12  4781  suceq  4943  xpeq1  5013  xpeq2  5014  csbxpgOLD  5081  rneq  5227  reseq1  5266  reseq2  5267  csbresgOLD  5276  resmpt  5322  imaeq1  5331  imaeq2  5332  mptcnv  5407  csbrngOLD  5468  dmpropg  5480  rnpropg  5487  cores  5509  cores2  5519  xpco  5546  iotaeq  5558  iotabi  5559  fntpg  5642  imain  5663  f1oprswap  5854  fveq1  5864  fveq2  5865  fvres  5879  csbfv12  5900  csbfv12gOLD  5901  fnimapr  5930  fvco2  5941  residpr  6064  fsnunfv  6100  fsnunres  6101  funiunfv  6147  fliftf  6200  isoini2  6222  riotaeqdv  6245  riotabidv  6246  riotauni  6250  riotabidva  6261  snriota  6274  oveq  6289  oveq1  6290  oveq2  6291  oprabbid  6333  mpt2eq123  6339  mpt2eq123dva  6341  mpt2eq3dva  6344  resmpt2  6383  ovres  6425  f1ocnvd  6507  ofeq  6525  ofreq  6526  fpar  6887  extmptsuppeq  6924  onovuni  7013  recseq  7043  tfr2a  7064  rdgeq1  7077  rdgeq2  7078  rdgsucmptf  7094  frsucmpt  7103  seqomeq12  7119  seqomsuc  7122  omopthi  7306  eceq1  7347  eceq2  7349  qseq1  7361  qseq2  7362  uniqs  7371  ecinxp  7386  qsinxp  7387  erovlem  7407  ecopovtrn  7414  ixpeq1  7480  supeq1  7904  supeq2  7907  supeq3  7908  supeq123d  7909  oieq1  7936  oieq2  7937  ordtypelem1  7942  inf3lemc  8042  wemapwe  8138  wemapweOLD  8139  r1sucg  8186  r1limg  8188  rankprb  8268  karden  8312  cardiun  8362  acneq  8423  alephlim  8447  alephsuc  8448  alephfplem2  8485  dfac2a  8509  infpssrlem2  8683  fin23lem34  8725  fin23lem35  8726  zorn2lem1  8875  zorn2lem7  8881  fpwwe2lem6  9012  fpwwe2lem13  9019  addpiord  9261  mulpiord  9262  addpqnq  9315  mulpqnq  9318  addassnq  9335  mulassnq  9336  distrnq  9338  lterpq  9347  ltexnq  9352  ltsrpr  9453  00sr  9475  recexsrlem  9479  mulgt0sr  9481  addcnsrec  9519  mulcnsrec  9520  negeq  9811  csbnegg  9816  negsubdi  9874  mulneg1  9992  deceq1  10978  deceq2  10979  xnegeq  11405  fseq1p1m1  11751  om2uzrdg  12034  uzrdgsuci  12038  seqeq1  12077  seqeq2  12078  seqeq3  12079  seqfeq4  12123  seqof  12131  hashprg  12427  hashmap  12458  hashbclem  12466  hashtpg  12488  csbwrdg  12535  s1eq  12574  cats1co  12783  s2eqd  12789  s3eqd  12790  s4eqd  12791  s5eqd  12792  s6eqd  12793  s7eqd  12794  s8eqd  12795  shftval  12869  limsupgle  13262  lo1eq  13353  rlimeq  13354  sumeq1  13473  sumeq2w  13476  sumeq2ii  13477  zsum  13502  sumss2  13510  fsumsplitsnun  13532  isumclim3  13536  fsumcom2  13551  fsumrev  13556  incexclem  13610  incexc2  13612  isumshft  13613  ef0lem  13675  ruclem7  13829  sadcp1  13963  smupp1  13988  smueqlem  13998  algrp1  14061  dfphi2  14162  prmdiveq  14174  pceulem  14227  vdwlem6  14362  cshwsiun  14441  setsid  14530  elbasfv  14536  elbasov  14537  imastset  14776  imasvscaval  14792  xpscg  14812  isoval  15019  funcoppc  15101  fulloppc  15148  fuccofval  15185  natpropd  15202  catccofval  15284  xpchomfval  15305  xpccofval  15308  lubfval  15464  glbfval  15477  grpidpropd  15764  gsumpropd2lem  15824  frmdplusg  15851  grpinvpropd  15920  grpsubpropd  15947  grpsubpropd2  15948  mulgpropd  15982  oppgmnd  16191  symgplusg  16216  sylow1lem2  16422  sylow3lem1  16450  prds1  17059  pwsmgp  17063  opprrng  17076  rngidpropd  17140  dvdsrpropd  17141  unitpropd  17142  invrpropd  17143  rhm1  17175  lmhmpropd  17514  lidlrsppropd  17672  lpival  17687  rrgsuppOLD  17727  ressascl  17780  asclpropd  17782  aspval2  17783  psrbas  17817  psrbasOLD  17818  psrplusg  17821  psrmulr  17824  psrvscafval  17830  resspsrbas  17857  ressmplbas2  17904  opsrle  17927  opsrbaslem  17929  mplrcl  17941  vr1val  18018  ressply1add  18058  ressply1mul  18059  ressply1vsca  18060  psrplusgpropd  18064  mplbaspropd  18065  psropprmul  18066  ply1baspropd  18071  ply1plusgpropd  18072  ply1sca2  18082  subrgvr1  18089  coe1mul2lem2  18096  ply1coe1eq  18127  zrhpropd  18335  znle  18356  frlmplusgval  18580  frlmvscafval  18582  mamudi  18688  mamudir  18689  matrcl  18697  oftpos  18737  mattpos1  18741  mdetfval  18871  mdetrlin  18887  mdetrsca  18888  mdetrsca2  18889  mdetrlin2  18892  mdetunilem5  18901  madufval  18922  madugsum  18928  idmatidpmat  19021  cpmidpmat  19157  cncmp  19674  2ndcsep  19742  llyeq  19753  nllyeq  19754  xkouni  19851  hmphindis  20049  pt1hmeo  20058  xkocnv  20066  ptcmplem2  20304  snclseqg  20365  prdstmdd  20373  ustexsym  20469  ucnextcn  20558  metreslem  20616  comet  20767  nrmmetd  20846  nmpropd  20865  isngp3  20869  ngpds  20874  subgnm  20898  tngnm  20916  idnghm  21001  cnmetdval  21029  cnmpt2pc  21179  htpyco2  21230  phtpyco2  21241  clsocv  21441  ovolunlem1a  21658  voliunlem3  21713  ioombl1lem4  21722  uniioombllem4  21746  itg11  21849  itgeq1f  21929  itgeq2  21935  iblss2  21963  itgss  21969  itgeqa  21971  itgfsum  21984  itgsplit  21993  ditgeq1  22003  ditgeq2  22004  ditgeq3  22005  dvcmulf  22099  dvmptfsum  22127  dvcnvrelem2  22170  mdegfval  22211  mdegpropd  22235  deg1propd  22237  plyeq0  22359  coe11  22400  dgrlt  22413  dgradd2  22415  dgrmulc  22418  dvply1  22430  fta1lem  22453  pserulm  22567  rlimcnp2  23040  jensenlem1  23060  basellem5  23102  dchrbas  23254  dchrrcl  23259  dchrplusg  23266  dchrfi  23274  lgsdi  23351  lgseisenlem2  23369  lgsquadlem3  23375  dchrmusumlema  23422  rpvmasum2  23441  dchrisum0lema  23443  pntlemg  23527  colperpexlem2  23826  axlowdimlem13  23949  isusgra0  24039  nbgraf1olem5  24137  nb3graprlem1  24143  constr2spthlem1  24288  constr3pthlem1  24347  constr3pthlem2  24348  wwlkextwrd  24420  rusgranumwlkl1  24639  rusgranumwlklem3  24643  numclwwlkovf2  24777  avril1  24863  0vfval  25191  imsval  25283  imsdval  25284  bcseqi  25729  normpythi  25751  cm0  26219  fh1  26228  pjcji  26294  opsqrlem5  26755  pjsdi2i  26768  pjclem3  26808  pjci  26811  golem1  26882  iunrdx  27120  ofresid  27171  resmptf  27185  f1od2  27235  gsumvsca1  27452  gsumvsca2  27453  rhmopp  27488  resv1r  27506  xrge0mulc1cn  27575  qqhval2  27615  esumeq12dvaf  27700  esumeq2  27705  esumf1o  27717  esumfzf  27731  esumss  27734  esumpfinvalf  27738  ofceq  27752  itgeq12dv  27924  ccatmulgnn0dir  28152  cvmliftlem5  28390  cvmliftlem10  28395  cvmlift2lem9  28412  cvmliftphtlem  28418  prodeq1f  28633  prodeq2w  28637  prodeq2ii  28638  zprod  28662  fprodm1s  28692  fprodp1s  28693  fprodshft  28699  fprodrev  28700  fprodcom2  28707  iprodclim3  28712  mpteq12d  28795  rdgprc  28820  dfrdg2  28821  predeq123  28838  trpredeq1  28896  trpredeq2  28897  trpredeq3  28898  wrecseq123  28930  wsuceq123  28963  wlimeq12  28968  symdifeq1  29063  symdifeq2  29064  altopthsn  29204  altxpeq1  29216  altxpeq2  29217  ee7.2aOLD  29519  finixpnum  29631  ptrest  29641  mbfposadd  29655  cnambfre  29656  iblabsnclem  29671  ftc1anclem1  29683  heiborlem4  29929  heiborlem6  29931  mpt2bi123f  30191  iineq12f  30193  mptbi12f  30195  imaiinfv  30245  mapfzcons1  30269  rexrabdioph  30347  dnnumch1  30610  dnwech  30614  aomclem6  30625  pwssplit4  30655  pwfi2f1o  30664  mendplusgfval  30755  mendvscafval  30760  dropab1  30950  dropab2  30951  itgsinexplem1  31287  wallispi2lem2  31388  afveq12d  31701  aoveq123d  31746  aovfundmoveq  31749  aovnuoveq  31759  aovvoveq  31760  aovovn0oveq  31762  resisresindm  31788  fsumsplitsndif  31829  xpprsng  32005  csbfv12gALTOLD  32710  csbima12gALTOLD  32711  bnj956  32923  bnj1385  32979  bnj96  33011  bnj548  33043  bnj553  33044  bnj554  33045  bnj602  33061  bnj18eq1  33073  bnj1234  33157  bnj1296  33165  bnj1318  33169  bnj1442  33193  bnj1450  33194  bj-rabbida2  33575  bj-sngleq  33615  bj-tageq  33624  bj-projeq  33640  bj-projval  33644  bj-1upleq  33647  bj-pr1eq  33650  bj-pr2eq  33664  riotaclbgBAD  33766  riotaclbBAD  33767  toycom  33779  ldualvbase  33932  ldualfvadd  33934  ldualsca  33938  ldualsbase  33939  ldualsaddN  33940  ldualfvs  33942  ldual0  33953  ldual1  33954  ldualneg  33955  cdleme19f  35113  cdleme20m  35128  cdleme21k  35143  cdleme27b  35173  cdleme31so  35184  cdleme31sn  35185  cdleme31se  35187  cdleme31se2  35188  cdleme31sc  35189  cdleme31sde  35190  cdleme31fv  35195  cdleme40v  35274  cdleme43dN  35297  cdlemeg46ngfr  35323  ltrnco4  35544  tgrpbase  35551  tgrpopr  35552  erngbase  35606  erngfplus  35607  erngfmul  35610  erngbase-rN  35614  erngfplus-rN  35615  erngfmul-rN  35618  dvasca  35811  dvavbase  35818  dvafvadd  35819  dvafvsca  35821  tendocnv  35827  dvhsca  35888  dvhfplusr  35890  dvhvbase  35893  dvhfvadd  35897  dvhfvsca  35906  lcdvadd  36403  lcdsbase  36406  lcdsadd  36407  lcdvs  36409  lcd0  36414  lcd1  36415  lcdneg  36416  mapdvalc  36435  mapdval4N  36438  xpcogend  36792