Theorem 3eqtr4g 2824

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
3eqtr4g.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr4g.2	⊢ 𝐶 = 𝐴
3eqtr4g.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3eqtr4g	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr4g

Step	Hyp	Ref	Expression
1		3eqtr4g.2	. . 3 ⊢ 𝐶 = 𝐴
2		3eqtr4g.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	eqtrid 2811	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eqtr4di 2817	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756

This theorem is referenced by:  rabbidva2  3418  rabbida4  3441  csbeq1  3857  csbeq2  3859  csbeq2d  3860  csbeq2dv  3861  difeq1  4075  difeq2  4076  uneq2  4117  ineq1  4167  ineq2  4168  symdifeq1  4209  symdifeq2  4210  dfrab3ss  4277  csbprc  4365  csbnestgfw  4378  csbnestgf  4383  disjssun  4424  ifeq1  4486  ifeq2  4487  pweqALT  4572  sneq  4594  csbsng  4669  csbprg  4670  preq1  4694  preq2  4695  tpeq1  4703  tpeq2  4704  tpeq3  4705  prprc1  4726  tpprceq3  4766  opeq1  4833  opeq2  4834  oteq1  4842  oteq2  4843  oteq3  4844  csbopg  4851  uniprg  4883  csbuni  4898  inteq  4910  iineq1  4969  iineq2  4972  iuneq12df  4978  iuneq12d  4981  dfiin2g  4990  iinrab  5028  iinin1  5038  iinxprg  5048  iununi  5058  opabbid  5167  opabbidv  5168  mpteq12da  5185  mpteq12f  5187  mpteq12dva  5188  csbmpt12  5530  xpeq1  5663  xpeq2  5670  rneq  5914  reseq1  5961  reseq2  5962  resima2  6004  resindmOLD  6019  resmpt  6028  resmptf  6030  imaeq1  6046  imaeq2  6047  mptcnv  6127  xpdisj1  6148  xpdisj2  6149  resdisj  6157  dmpropg  6204  rnpropg  6211  cores  6238  cores2  6249  xpco  6278  predeq123  6291  csbpredg  6296  sspred  6299  predres  6328  suceqd  6415  sucprc  6426  iotaeq  6491  iotabi  6492  fntpg  6583  imain  6608  f1oprswap  6854  fveq1  6868  fveq2  6869  fvres  6888  csbfv12  6914  fnimapr  6952  fnimatpd  6953  fvco2  6966  xpprsng  7124  residpr  7127  fsnunfv  7173  fsnunres  7174  funiunfv  7234  f1ofvswap  7292  fliftf  7301  isoini2  7325  eqfunressuc  7347  riotaeqdv  7356  riotabidv  7357  riotauni  7361  riotabidva  7374  snriota  7388  oveq  7404  oveq1  7405  oveq2  7406  oprabbid  7463  oprabbidv  7464  mpoeq123  7470  mpoeq123dva  7472  mpoeq3dva  7475  resmpo  7518  ovres  7564  f1ocnvd  7649  ofeqd  7664  ofreq  7666  fpar  8097  frecseq123  8265  csbfrecsg  8267  wrecseq123  8296  csbwrecsg  8301  onovuni  8315  recseq  8346  tfr2a  8368  rdgeq1  8384  rdgeq2  8385  rdgsucmptf  8401  frsucmpt  8411  seqomeq12  8427  seqomsuc  8430  omopthi  8633  eceq1  8720  eceq2  8722  qseq1  8740  qseq2  8741  uniqs  8757  snecg  8761  ecinxp  8776  qsinxp  8777  erovlem  8797  ecopovtrn  8804  ixpeq1  8892  unfi  9141  supeq1  9393  supeq2  9396  supeq3  9397  supeq123d  9398  infeq1  9425  infeq2  9428  infeq3  9429  infeq123d  9430  infiso  9458  oieq1  9462  oieq2  9463  ordtypelem1  9468  inf3lemc  9583  wemapwe  9654  ttrcleq  9666  r1sucg  9729  r1limg  9731  rankprb  9811  karden  9855  djueq12  9864  cardiun  9942  acneq  10001  alephlim  10025  alephsuc  10026  alephfplem2  10063  infpssrlem2  10263  fin23lem34  10305  fin23lem35  10306  zorn2lem1  10455  zorn2lem7  10461  fpwwe2lem5  10595  fpwwe2lem12  10602  addpiord  10844  mulpiord  10845  addpqnq  10898  mulpqnq  10901  addassnq  10918  mulassnq  10919  distrnq  10921  lterpq  10930  ltexnq  10935  ltsrpr  11037  00sr  11059  recexsrlem  11063  mulgt0sr  11065  addcnsrec  11103  mulcnsrec  11104  negeq  11424  csbnegg  11429  negsubdi  11489  mulneg1  11625  negfi  12143  deceq1  12695  deceq2  12696  xnegeq  13212  fseq1p1m1  13605  om2uzrdg  13971  uzrdgsuci  13975  seqeq1  14019  seqeq2  14020  seqeq3  14021  seqfeq4  14066  seqof  14074  hashprg  14410  hashtpg  14500  csbwrdg  14559  s1eq  14616  cats1co  14871  s2eqd  14878  s3eqd  14879  s4eqd  14880  s5eqd  14881  s6eqd  14882  s7eqd  14883  s8eqd  14884  xpcogend  14989  shftval  15089  limsupgle  15506  lo1eq  15597  rlimeq  15598  sumeq1  15718  sumeq2w  15721  sumeq2ii  15722  sumeq2sdv  15732  zsum  15747  sumss2  15755  fsumsplitsnun  15784  isumclim3  15788  fsumcom2  15803  incexclem  15868  incexc2  15870  isumshft  15871  prodeq1f  15938  prodeq1  15939  prodeq2w  15942  prodeq2ii  15943  prodeq2sdv  15955  zprod  15969  fprodm1s  16002  fprodp1s  16003  fprodcom2  16016  fprodsplitf  16020  iprodclim3  16032  ef0lem  16110  ruclem7  16270  sadcp1  16491  smupp1  16516  smueqlem  16526  algrp1  16610  dfphi2  16811  prmdiveq  16823  pceulem  16883  vdwlem6  17024  cshwsiun  17137  sloteq  17221  setsid  17245  elbasfv  17253  elbasov  17254  imastset  17554  imasvscaval  17570  isoval  17800  funcoppc  17910  fulloppc  17959  fuccofval  17997  natpropd  18014  catccofval  18139  xpchomfval  18213  xpccofval  18216  lubfval  18382  glbfval  18395  chneq1  18646  chneq2  18647  grpidpropd  18698  gsumpropd2lem  18715  frmdplusg  18890  efmndplusg  18916  grpinvpropd  19059  grpsubpropd  19089  grpsubpropd2  19090  mulgpropd  19160  ecqusaddd  19235  oppgmnd  19396  sylow1lem2  19641  sylow3lem1  19669  prds1  20373  pwsmgp  20377  opprrng  20396  rngidpropd  20466  dvdsrpropd  20467  unitpropd  20468  invrpropd  20469  rhm1  20540  rhmopp  20561  rhmsubclem2  20738  lmhmpropd  21142  lidlrsppropd  21316  rngqiprnglinlem2  21364  lpival  21396  pzriprnglem11  21545  zrhpropd  21568  znle  21590  frlmplusgval  21818  frlmvscafval  21820  ressascl  21950  asclpropd  21951  aspval2  21952  psrbas  21988  psrplusg  21991  psrmulr  21996  psrvscafval  22002  resspsrbas  22027  ressmplbas2  22081  opsrle  22102  opsrbaslem  22104  vr1val  22256  ressply1add  22293  ressply1mul  22294  ressply1vsca  22295  psrplusgpropd  22299  mplbaspropd  22300  psropprmul  22301  ply1baspropd  22306  ply1plusgpropd  22307  ply1sca2  22317  ply1ascl0  22318  ply1ascl1  22319  subrgvr1  22326  coe1mul2lem2  22333  ply1coe1eq  22365  evls1addd  22436  evls1muld  22437  evls1vsca  22438  rhmply1vr1  22449  rhmply1vsca  22450  mamudi  22465  mamudir  22466  matrcl  22474  oftpos  22514  mattpos1  22518  mdetfval  22648  mdetrlin  22664  mdetrsca  22665  mdetrsca2  22666  mdetrlin2  22669  mdetunilem5  22678  madufval  22699  madugsum  22705  idmatidpmat  22799  cpmidpmat  22935  cncmp  23454  2ndcsep  23521  llyeq  23532  nllyeq  23533  xkouni  23661  hmphindis  23859  xkocnv  23876  ptcmplem2  24115  snclseqg  24178  prdstmdd  24186  ustexsym  24278  ucnextcn  24365  metreslem  24424  comet  24575  nrmmetd  24636  nmpropd  24656  isngp3  24660  ngpds  24666  subgnm  24695  tngnm  24713  idnghm  24805  cnmetdval  24832  cnmpopc  24992  htpyco2  25043  phtpyco2  25054  clsocv  25314  rrxprds  25453  rrxnm  25455  rrxplusgvscavalb  25459  ovolunlem1a  25560  voliunlem3  25616  ioombl1lem4  25625  uniioombllem4  25650  itg11  25755  itgeq1f  25835  itgeq1fOLD  25836  itgeq1  25837  itgeq2  25842  iblss2  25870  itgss  25876  itgeqa  25878  itgfsum  25891  itgsplit  25900  ditgeq1  25912  ditgeq2  25913  ditgeq3  25914  dvcmulf  26009  dvmptfsum  26039  dvcnvrelem2  26082  mdegfval  26124  mdegpropd  26146  deg1propd  26148  plyeq0  26273  coe11  26315  dgrlt  26328  dgradd2  26330  dgrmulc  26333  dvply1  26350  fta1lem  26373  pserulm  26487  rlimcnp2  27033  jensenlem1  27053  basellem5  27151  dchrbas  27301  dchrrcl  27306  dchrplusg  27313  dchrfi  27321  lgsdi  27400  lgseisenlem2  27442  lgsquadlem3  27448  dchrmusumlema  27559  rpvmasum2  27578  dchrisum0lema  27580  pntlemg  27664  nosupbnd2lem1  27781  lruneq  28002  addsval  28057  mulsval  28204  seqseq123d  28381  colperpexlem2  28906  axlowdimlem13  29157  uhgrvtxedgiedgb  29339  nb3grprlem1  29583  crctcshlem2  30020  wpthswwlks2on  30166  clwlknf1oclwwlkn  30288  frgrncvvdeq  30513  avril1  30667  0vfval  30811  imsval  30890  imsdval  30891  bcseqi  31325  normpythi  31347  cm0  31814  fh1  31823  pjcji  31889  opsqrlem5  32349  pjsdi2i  32362  pjclem3  32402  pjci  32405  golem1  32476  iuneq12daf  32758  iunrdx  32765  ofresid  32846  cnvprop  32900  coprprop  32903  f1od2  32923  dp2eq1  33052  dp2eq2  33053  fzto1st1  33284  gsumvsca1  33408  gsumvsca2  33409  urpropd  33413  resv1r  33527  nsgqusf1olem2  33602  oppr2idl  33676  opprqus0g  33680  ressply1evls1  33763  esplyfvn  33876  vietalem  33878  lindsunlem  33923  fedgmullem1  33928  fedgmullem2  33929  fedgmul  33930  fldsdrgfldext2  33961  fldextrspunlem1  33974  fldextrspunfld  33975  algextdeglem4  34019  crefeq  34144  rspectopn  34166  xrge0mulc1cn  34240  qqhval2  34281  esumeq12dvaf  34330  esumeq2  34335  esumf1o  34349  esumfzf  34368  esumss  34371  esumpfinvalf  34375  ofceq  34396  carsgclctunlem1  34616  itgeq12dv  34625  ccatmulgnn0dir  34841  breprexpnat  34930  bnj956  35074  bnj1385  35129  bnj96  35162  bnj548  35194  bnj553  35195  bnj554  35196  bnj602  35212  bnj18eq1  35224  bnj1234  35310  bnj1296  35318  bnj1318  35322  bnj1442  35346  bnj1450  35347  cvmliftlem5  35644  cvmliftlem10  35649  cvmlift2lem9  35666  cvmliftphtlem  35672  satfdm  35724  mthmpps  35937  rdgprc  36147  dfrdg2  36148  wsuceq123  36167  wlimeq12  36172  altopthsn  36316  altxpeq1  36328  altxpeq2  36329  nmulprop  36545  ixpeq12dv  36581  prodeq12sdv  36583  itgeq12sdv  36584  ditgeq123dv  36586  cbvcsbdavw  36624  cbvcsbdavw2  36625  cbvrabdavw  36626  cbviundavw  36627  cbviindavw  36628  cbvopab1davw  36629  cbvopab2davw  36630  cbvopabdavw  36631  cbvmptdavw  36632  cbviotadavw  36634  cbvriotadavw  36635  cbvoprab1davw  36636  cbvoprab2davw  36637  cbvoprab3davw  36638  cbvoprab123davw  36639  cbvoprab12davw  36640  cbvoprab23davw  36641  cbvoprab13davw  36642  cbvixpdavw  36643  cbvsumdavw  36644  cbvproddavw  36645  cbvitgdavw  36646  cbvditgdavw  36647  cbvrabdavw2  36650  cbviundavw2  36651  cbviindavw2  36652  cbvmptdavw2  36653  cbvriotadavw2  36655  cbvmpodavw2  36656  cbvmpo1davw2  36657  cbvmpo2davw2  36658  cbvixpdavw2  36659  cbvsumdavw2  36660  cbvproddavw2  36661  cbvitgdavw2  36662  cbvditgdavw2  36663  ee7.2aOLD  36826  ttceq  36853  bj-sngleq  37457  bj-tageq  37466  bj-projeq  37482  bj-projval  37486  bj-1upleq  37489  bj-pr1eq  37492  bj-pr2eq  37506  bj-evaleq  37566  bj-imafv  37748  csbrecsg  37827  csbrdgg  37828  csboprabg  37829  csbmpo123  37830  finxpeq1  37885  finxpeq2  37886  csbfinxpg  37887  finxpreclem4  37893  cureq  38100  unceq  38101  uncov  38105  unccur  38107  finixpnum  38109  ptrest  38123  poimirlem3  38127  poimirlem9  38133  poimirlem15  38139  poimirlem16  38140  poimirlem26  38150  poimirlem27  38151  mbfposadd  38171  cnambfre  38172  iblabsnclem  38187  ftc1anclem1  38197  heiborlem4  38318  heiborlem6  38320  mpobi123f  38666  iineq12f  38668  mptbi12f  38670  eccnvepres  38790  xrneq1  38900  xrneq2  38903  shiftstableeq2  38987  cosseq  39020  redundss3  39216  riotaclbgBAD  39583  toycom  39602  ldualvbase  39755  ldualfvadd  39757  ldualsca  39761  ldualsbase  39762  ldualsaddN  39763  ldualfvs  39765  ldual0  39776  ldual1  39777  ldualneg  39778  cdleme19f  40937  cdleme20m  40952  cdleme21k  40967  cdleme27b  40997  cdleme31so  41008  cdleme31sn  41009  cdleme31se  41011  cdleme31se2  41012  cdleme31sc  41013  cdleme31sde  41014  cdleme31fv  41019  cdleme40v  41098  cdleme43dN  41121  cdlemeg46ngfr  41147  ltrnco4  41368  tgrpbase  41375  tgrpopr  41376  erngbase  41430  erngfplus  41431  erngfmul  41434  erngbase-rN  41438  erngfplus-rN  41439  erngfmul-rN  41442  dvasca  41635  dvavbase  41642  dvafvadd  41643  dvafvsca  41645  tendocnv  41650  dvhsca  41711  dvhfplusr  41713  dvhvbase  41716  dvhfvadd  41720  dvhfvsca  41729  lcdvadd  42226  lcdsbase  42229  lcdsadd  42230  lcdvs  42232  lcd0  42237  lcd1  42238  lcdneg  42239  fsuppind  43177  imaiinfv  43279  mapfzcons1  43303  rexrabdioph  43376  dnnumch1  43626  dnwech  43630  aomclem6  43641  pwssplit4  43671  pwfi2f1o  43678  mendplusgfval  43763  mendvscafval  43768  harval3  44119  dssmapntrcls  44709  scotteqd  44818  colleq12d  44834  uzmptshftfval  44927  dropab1  45027  dropab2  45028  iineq12dv  45689  rabbida2  45715  rabbida3  45718  itgsinexplem1  46533  wallispi2lem2  46651  fourierdlem36  46722  etransclem4  46817  fcoreslem1  47662  afveq12d  47732  aoveq123d  47777  aovfundmoveq  47780  aovnuoveq  47790  aovvoveq  47791  aovovn0oveq  47793  afv2eq12d  47814  fsumsplitsndif  47980  rngccofvalALTV  48897  rhmsubcALTVlem2  48909  ringccofvalALTV  48931  itscnhlinecirc02plem2  49410  oppfrcl3  49756  oppf1st2nd  49757  uppropd  49807  natoppf  49855  catcrcl  50021  lmdpropd  50283  cmdpropd  50284  lmddu  50293  cmddu  50294  setrecseq  50311  aacllem  50427