Theorem 3eqtr4g 2796

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 2783	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eqtr4di 2789	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  rabbidva2  3391  rabbida4  3414  csbeq1  3840  csbeq2  3842  csbeq2d  3843  csbeq2dv  3844  difeq1  4059  difeq2  4060  uneq2  4102  ineq1  4153  ineq2  4154  symdifeq1  4195  symdifeq2  4196  dfrab3ss  4263  csbprc  4349  csbnestgfw  4362  csbnestgf  4367  disjssun  4408  ifeq1  4470  ifeq2  4471  pweqALT  4556  sneq  4577  csbsng  4652  csbprg  4653  preq1  4677  preq2  4678  tpeq1  4686  tpeq2  4687  tpeq3  4688  prprc1  4709  tpprceq3  4749  opeq1  4816  opeq2  4817  oteq1  4825  oteq2  4826  oteq3  4827  csbopg  4834  uniprg  4866  csbuni  4880  inteq  4892  iineq1  4951  iineq2  4954  iuneq12df  4960  iuneq12d  4963  dfiin2g  4973  iinrab  5011  iinin1  5021  iinxprg  5031  iununi  5041  opabbid  5150  opabbidv  5151  mpteq12da  5168  mpteq12f  5170  mpteq12dva  5171  csbmpt12  5512  xpeq1  5645  xpeq2  5652  rneq  5891  reseq1  5938  reseq2  5939  resima2  5981  resindm  5995  resmpt  6002  resmptf  6004  imaeq1  6020  imaeq2  6021  mptcnv  6102  xpdisj1  6125  xpdisj2  6126  resdisj  6133  dmpropg  6179  rnpropg  6186  cores  6213  cores2  6224  xpco  6253  predeq123  6266  csbpredg  6271  sspred  6274  predres  6303  suceqd  6390  sucprc  6401  iotaeq  6466  iotabi  6467  fntpg  6558  imain  6583  f1oprswap  6825  fveq1  6839  fveq2  6840  fvres  6859  csbfv12  6885  fnimapr  6923  fnimatpd  6924  fvco2  6937  xpprsng  7093  residpr  7096  fsnunfv  7142  fsnunres  7143  funiunfv  7203  f1ofvswap  7261  fliftf  7270  isoini2  7294  eqfunressuc  7316  riotaeqdv  7325  riotabidv  7326  riotauni  7330  riotabidva  7343  snriota  7357  oveq  7373  oveq1  7374  oveq2  7375  oprabbid  7432  oprabbidv  7433  mpoeq123  7439  mpoeq123dva  7441  mpoeq3dva  7444  resmpo  7487  ovres  7533  f1ocnvd  7618  ofeqd  7633  ofreq  7635  fpar  8066  frecseq123  8232  csbfrecsg  8234  wrecseq123  8263  csbwrecsg  8268  onovuni  8282  recseq  8313  tfr2a  8334  rdgeq1  8350  rdgeq2  8351  rdgsucmptf  8367  frsucmpt  8377  seqomeq12  8393  seqomsuc  8396  omopthi  8597  eceq1  8683  eceq2  8685  qseq1  8703  qseq2  8704  uniqs  8720  snecg  8724  ecinxp  8739  qsinxp  8740  erovlem  8760  ecopovtrn  8767  ixpeq1  8856  unfi  9105  supeq1  9358  supeq2  9361  supeq3  9362  supeq123d  9363  infeq1  9390  infeq2  9393  infeq3  9394  infeq123d  9395  infiso  9423  oieq1  9427  oieq2  9428  ordtypelem1  9433  inf3lemc  9547  wemapwe  9618  ttrcleq  9630  r1sucg  9693  r1limg  9695  rankprb  9775  karden  9819  djueq12  9828  cardiun  9906  acneq  9965  alephlim  9989  alephsuc  9990  alephfplem2  10027  infpssrlem2  10226  fin23lem34  10268  fin23lem35  10269  zorn2lem1  10418  zorn2lem7  10424  fpwwe2lem5  10558  fpwwe2lem12  10565  addpiord  10807  mulpiord  10808  addpqnq  10861  mulpqnq  10864  addassnq  10881  mulassnq  10882  distrnq  10884  lterpq  10893  ltexnq  10898  ltsrpr  11000  00sr  11022  recexsrlem  11026  mulgt0sr  11028  addcnsrec  11066  mulcnsrec  11067  negeq  11385  csbnegg  11390  negsubdi  11450  mulneg1  11586  negfi  12105  deceq1  12649  deceq2  12650  xnegeq  13159  fseq1p1m1  13552  om2uzrdg  13918  uzrdgsuci  13922  seqeq1  13966  seqeq2  13967  seqeq3  13968  seqfeq4  14013  seqof  14021  hashprg  14357  hashtpg  14447  csbwrdg  14506  s1eq  14563  cats1co  14818  s2eqd  14825  s3eqd  14826  s4eqd  14827  s5eqd  14828  s6eqd  14829  s7eqd  14830  s8eqd  14831  xpcogend  14936  shftval  15036  limsupgle  15439  lo1eq  15530  rlimeq  15531  sumeq1  15651  sumeq2w  15654  sumeq2ii  15655  sumeq2sdv  15665  zsum  15680  sumss2  15688  fsumsplitsnun  15717  isumclim3  15721  fsumcom2  15736  incexclem  15801  incexc2  15803  isumshft  15804  prodeq1f  15871  prodeq1  15872  prodeq2w  15875  prodeq2ii  15876  prodeq2sdv  15888  zprod  15902  fprodm1s  15935  fprodp1s  15936  fprodcom2  15949  fprodsplitf  15953  iprodclim3  15965  ef0lem  16043  ruclem7  16203  sadcp1  16424  smupp1  16449  smueqlem  16459  algrp1  16543  dfphi2  16744  prmdiveq  16756  pceulem  16816  vdwlem6  16957  cshwsiun  17070  sloteq  17153  setsid  17177  elbasfv  17185  elbasov  17186  imastset  17486  imasvscaval  17502  isoval  17732  funcoppc  17842  fulloppc  17891  fuccofval  17929  natpropd  17946  catccofval  18071  xpchomfval  18145  xpccofval  18148  lubfval  18314  glbfval  18327  chneq1  18578  chneq2  18579  grpidpropd  18630  gsumpropd2lem  18647  frmdplusg  18822  efmndplusg  18848  grpinvpropd  18991  grpsubpropd  19021  grpsubpropd2  19022  mulgpropd  19092  ecqusaddd  19167  oppgmnd  19329  sylow1lem2  19574  sylow3lem1  19602  prds1  20302  pwsmgp  20306  opprrng  20325  rngidpropd  20395  dvdsrpropd  20396  unitpropd  20397  invrpropd  20398  rhm1  20468  rhmopp  20486  rhmsubclem2  20663  lmhmpropd  21068  lidlrsppropd  21242  rngqiprnglinlem2  21290  lpival  21322  pzriprnglem11  21471  zrhpropd  21494  znle  21516  frlmplusgval  21744  frlmvscafval  21746  ressascl  21876  asclpropd  21877  aspval2  21878  psrbas  21913  psrplusg  21916  psrmulr  21921  psrvscafval  21927  resspsrbas  21952  ressmplbas2  22005  opsrle  22025  opsrbaslem  22027  vr1val  22155  ressply1add  22193  ressply1mul  22194  ressply1vsca  22195  psrplusgpropd  22199  mplbaspropd  22200  psropprmul  22201  ply1baspropd  22206  ply1plusgpropd  22207  ply1sca2  22217  ply1ascl0  22218  ply1ascl1  22219  subrgvr1  22226  coe1mul2lem2  22233  ply1coe1eq  22265  evls1addd  22336  evls1muld  22337  evls1vsca  22338  rhmply1vr1  22352  rhmply1vsca  22353  mamudi  22368  mamudir  22369  matrcl  22377  oftpos  22417  mattpos1  22421  mdetfval  22551  mdetrlin  22567  mdetrsca  22568  mdetrsca2  22569  mdetrlin2  22572  mdetunilem5  22581  madufval  22602  madugsum  22608  idmatidpmat  22702  cpmidpmat  22838  cncmp  23357  2ndcsep  23424  llyeq  23435  nllyeq  23436  xkouni  23564  hmphindis  23762  xkocnv  23779  ptcmplem2  24018  snclseqg  24081  prdstmdd  24089  ustexsym  24181  ucnextcn  24268  metreslem  24327  comet  24478  nrmmetd  24539  nmpropd  24559  isngp3  24563  ngpds  24569  subgnm  24598  tngnm  24616  idnghm  24708  cnmetdval  24735  cnmpopc  24895  htpyco2  24946  phtpyco2  24957  clsocv  25217  rrxprds  25356  rrxnm  25358  rrxplusgvscavalb  25362  ovolunlem1a  25463  voliunlem3  25519  ioombl1lem4  25528  uniioombllem4  25553  itg11  25658  itgeq1f  25738  itgeq1fOLD  25739  itgeq1  25740  itgeq2  25745  iblss2  25773  itgss  25779  itgeqa  25781  itgfsum  25794  itgsplit  25803  ditgeq1  25815  ditgeq2  25816  ditgeq3  25817  dvcmulf  25912  dvmptfsum  25942  dvcnvrelem2  25985  mdegfval  26027  mdegpropd  26049  deg1propd  26051  plyeq0  26176  coe11  26218  dgrlt  26231  dgradd2  26233  dgrmulc  26236  dvply1  26250  fta1lem  26273  pserulm  26387  rlimcnp2  26930  jensenlem1  26950  basellem5  27048  dchrbas  27198  dchrrcl  27203  dchrplusg  27210  dchrfi  27218  lgsdi  27297  lgseisenlem2  27339  lgsquadlem3  27345  dchrmusumlema  27456  rpvmasum2  27475  dchrisum0lema  27477  pntlemg  27561  nosupbnd2lem1  27679  lruneq  27899  addsval  27954  mulsval  28101  seqseq123d  28278  colperpexlem2  28799  axlowdimlem13  29023  uhgrvtxedgiedgb  29205  nb3grprlem1  29449  crctcshlem2  29886  wpthswwlks2on  30032  clwlknf1oclwwlkn  30154  frgrncvvdeq  30379  avril1  30533  0vfval  30677  imsval  30756  imsdval  30757  bcseqi  31191  normpythi  31213  cm0  31680  fh1  31689  pjcji  31755  opsqrlem5  32215  pjsdi2i  32228  pjclem3  32268  pjci  32271  golem1  32342  iuneq12daf  32626  iunrdx  32633  ofresid  32715  cnvprop  32769  coprprop  32772  f1od2  32792  dp2eq1  32932  dp2eq2  32933  fzto1st1  33163  gsumvsca1  33287  gsumvsca2  33288  urpropd  33292  resv1r  33399  nsgqusf1olem2  33474  oppr2idl  33546  opprqus0g  33550  ressply1evls1  33625  esplyfvn  33721  vietalem  33723  lindsunlem  33768  fedgmullem1  33773  fedgmullem2  33774  fedgmul  33775  fldsdrgfldext2  33806  fldextrspunlem1  33819  fldextrspunfld  33820  algextdeglem4  33864  crefeq  33989  rspectopn  34011  xrge0mulc1cn  34085  qqhval2  34126  esumeq12dvaf  34175  esumeq2  34180  esumf1o  34194  esumfzf  34213  esumss  34216  esumpfinvalf  34220  ofceq  34241  carsgclctunlem1  34461  itgeq12dv  34470  ccatmulgnn0dir  34686  breprexpnat  34778  bnj956  34919  bnj1385  34974  bnj96  35007  bnj548  35039  bnj553  35040  bnj554  35041  bnj602  35057  bnj18eq1  35069  bnj1234  35155  bnj1296  35163  bnj1318  35167  bnj1442  35191  bnj1450  35192  cvmliftlem5  35471  cvmliftlem10  35476  cvmlift2lem9  35493  cvmliftphtlem  35499  satfdm  35551  mthmpps  35764  rdgprc  35974  dfrdg2  35975  wsuceq123  35994  wlimeq12  35999  altopthsn  36143  altxpeq1  36155  altxpeq2  36156  ixpeq12dv  36398  prodeq12sdv  36400  itgeq12sdv  36401  ditgeq123dv  36403  cbvcsbdavw  36441  cbvcsbdavw2  36442  cbvrabdavw  36443  cbviundavw  36444  cbviindavw  36445  cbvopab1davw  36446  cbvopab2davw  36447  cbvopabdavw  36448  cbvmptdavw  36449  cbviotadavw  36451  cbvriotadavw  36452  cbvoprab1davw  36453  cbvoprab2davw  36454  cbvoprab3davw  36455  cbvoprab123davw  36456  cbvoprab12davw  36457  cbvoprab23davw  36458  cbvoprab13davw  36459  cbvixpdavw  36460  cbvsumdavw  36461  cbvproddavw  36462  cbvitgdavw  36463  cbvditgdavw  36464  cbvrabdavw2  36467  cbviundavw2  36468  cbviindavw2  36469  cbvmptdavw2  36470  cbvriotadavw2  36472  cbvmpodavw2  36473  cbvmpo1davw2  36474  cbvmpo2davw2  36475  cbvixpdavw2  36476  cbvsumdavw2  36477  cbvproddavw2  36478  cbvitgdavw2  36479  cbvditgdavw2  36480  ee7.2aOLD  36643  ttceq  36670  bj-sngleq  37274  bj-tageq  37283  bj-projeq  37299  bj-projval  37303  bj-1upleq  37306  bj-pr1eq  37309  bj-pr2eq  37323  bj-evaleq  37383  bj-imafv  37565  csbrecsg  37644  csbrdgg  37645  csboprabg  37646  csbmpo123  37647  finxpeq1  37702  finxpeq2  37703  csbfinxpg  37704  finxpreclem4  37710  cureq  37917  unceq  37918  uncov  37922  unccur  37924  finixpnum  37926  ptrest  37940  poimirlem3  37944  poimirlem9  37950  poimirlem15  37956  poimirlem16  37957  poimirlem26  37967  poimirlem27  37968  mbfposadd  37988  cnambfre  37989  iblabsnclem  38004  ftc1anclem1  38014  heiborlem4  38135  heiborlem6  38137  mpobi123f  38483  iineq12f  38485  mptbi12f  38487  eccnvepres  38607  xrneq1  38717  xrneq2  38720  shiftstableeq2  38804  cosseq  38837  redundss3  39033  riotaclbgBAD  39400  toycom  39419  ldualvbase  39572  ldualfvadd  39574  ldualsca  39578  ldualsbase  39579  ldualsaddN  39580  ldualfvs  39582  ldual0  39593  ldual1  39594  ldualneg  39595  cdleme19f  40754  cdleme20m  40769  cdleme21k  40784  cdleme27b  40814  cdleme31so  40825  cdleme31sn  40826  cdleme31se  40828  cdleme31se2  40829  cdleme31sc  40830  cdleme31sde  40831  cdleme31fv  40836  cdleme40v  40915  cdleme43dN  40938  cdlemeg46ngfr  40964  ltrnco4  41185  tgrpbase  41192  tgrpopr  41193  erngbase  41247  erngfplus  41248  erngfmul  41251  erngbase-rN  41255  erngfplus-rN  41256  erngfmul-rN  41259  dvasca  41452  dvavbase  41459  dvafvadd  41460  dvafvsca  41462  tendocnv  41467  dvhsca  41528  dvhfplusr  41530  dvhvbase  41533  dvhfvadd  41537  dvhfvsca  41546  lcdvadd  42043  lcdsbase  42046  lcdsadd  42047  lcdvs  42049  lcd0  42054  lcd1  42055  lcdneg  42056  fsuppind  43023  imaiinfv  43125  mapfzcons1  43149  rexrabdioph  43222  dnnumch1  43472  dnwech  43476  aomclem6  43487  pwssplit4  43517  pwfi2f1o  43524  mendplusgfval  43609  mendvscafval  43614  harval3  43965  dssmapntrcls  44555  scotteqd  44664  colleq12d  44680  uzmptshftfval  44773  dropab1  44873  dropab2  44874  iineq12dv  45536  rabbida2  45562  rabbida3  45565  itgsinexplem1  46382  wallispi2lem2  46500  fourierdlem36  46571  etransclem4  46666  fcoreslem1  47511  afveq12d  47581  aoveq123d  47626  aovfundmoveq  47629  aovnuoveq  47639  aovvoveq  47640  aovovn0oveq  47642  afv2eq12d  47663  fsumsplitsndif  47829  rngccofvalALTV  48746  rhmsubcALTVlem2  48758  ringccofvalALTV  48780  itscnhlinecirc02plem2  49259  oppfrcl3  49605  oppf1st2nd  49606  uppropd  49656  natoppf  49704  catcrcl  49870  lmdpropd  50132  cmdpropd  50133  lmddu  50142  cmddu  50143  setrecseq  50160  aacllem  50276