Theorem 3eqtr4g 2822

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754

This theorem is used by:  rabbidva2  3416  rabbida4  3439  csbeq1  3853  csbeq2  3855  csbeq2d  3856  csbeq2dv  3857  difeq1  4070  difeq2  4071  uneq2  4112  ineq1  4162  ineq2  4163  symdifeq1  4204  symdifeq2  4205  dfrab3ss  4272  csbprc  4370  csbnestgfw  4383  csbnestgf  4388  disjssun  4424  ifeq1  4489  ifeq2  4490  pweqALT  4575  sneq  4597  csbsng  4672  csbprg  4673  preq1  4697  preq2  4698  tpeq1  4706  tpeq2  4707  tpeq3  4708  prprc1  4729  tpprceq3  4770  opeq1  4836  opeq2  4837  oteq1  4845  oteq2  4846  oteq3  4847  csbopg  4854  uniprg  4886  csbuni  4901  inteq  4913  iineq1  4972  iineq2  4975  iuneq12df  4981  iuneq12d  4984  dfiin2g  4993  iinrab  5031  iinin1  5043  iinxprg  5053  iununi  5063  opabbid  5174  opabbidv  5175  mpteq12da  5192  mpteq12f  5194  mpteq12dva  5195  csbmpt12  5540  xpeq1  5673  xpeq2  5680  rneq  5924  reseq1  5970  reseq2  5971  resima2  6013  resindmOLD  6028  resmpt  6037  resmptf  6039  imaeq1  6055  imaeq2  6056  mptcnv  6136  xpdisj1  6157  xpdisj2  6158  resdisj  6166  dmpropg  6215  rnpropg  6222  cores  6249  cores2  6260  xpco  6291  predeq123  6304  csbpredg  6309  sspred  6312  predres  6341  suceqd  6429  sucprc  6440  iotaeq  6505  iotabi  6506  fntpg  6597  imain  6622  f1oprswap  6867  fveq1  6881  fveq2  6882  fvres  6901  csbfv12  6927  fnimapr  6965  fnimatpd  6966  fvco2  6979  xpprsng  7138  xpsnprg  7139  xpsntpg  7140  residpr  7142  fsnunfv  7188  fsnunres  7189  funiunfv  7248  f1ofvswap  7310  fliftf  7319  isoini2  7343  eqfunressuc  7367  riotaeqdv  7374  riotabidv  7375  riotauni  7379  riotabidva  7392  snriota  7406  oveq  7422  oveq1  7423  oveq2  7424  oprabbid  7481  oprabbidv  7482  mpoeq123  7488  mpoeq123dva  7490  mpoeq3dva  7493  resmpo  7536  ovres  7582  f1ocnvd  7668  ofeqd  7683  ofreq  7685  fpar  8116  frecseq123  8284  csbfrecsg  8286  wrecseq123  8315  csbwrecsg  8320  onovuni  8334  recseq  8365  tfr2a  8387  rdgeq1  8403  rdgeq2  8404  rdgsucmptf  8420  frsucmpt  8430  seqomeq12  8446  seqomsuc  8449  omopthi  8652  eceq1  8739  eceq2  8741  qseq1  8759  qseq2  8760  uniqs  8776  snecg  8780  ecinxp  8795  qsinxp  8796  erovlem  8816  ecopovtrn  8823  cureq  8871  uncov  8875  ixpeq1  8918  unfi  9168  supeq1  9418  supeq2  9421  supeq3  9422  supeq123d  9423  infeq1  9450  infeq2  9453  infeq3  9454  infeq123d  9455  infiso  9483  oieq1  9487  oieq2  9488  ordtypelem1  9493  inf3lemc  9608  wemapwe  9679  ttrcleq  9691  r1sucg  9754  r1limg  9756  rankprb  9836  scotteqd  9872  karden  9901  kardenOLD  9902  djueq12  9912  cardiun  9990  acneq  10049  alephlim  10073  alephsuc  10074  alephfplem2  10111  infpssrlem2  10309  fin23lem34  10351  fin23lem35  10352  zorn2lem1  10501  zorn2lem7  10507  fpwwe2lem5  10645  fpwwe2lem12  10652  addpiord  10894  mulpiord  10895  addpqnq  10948  mulpqnq  10951  addassnq  10968  mulassnq  10969  distrnq  10971  lterpq  10980  ltexnq  10985  ltsrpr  11087  00sr  11109  recexsrlem  11113  mulgt0sr  11115  addcnsrec  11153  mulcnsrec  11154  negeq  11474  csbnegg  11479  negsubdi  11539  mulneg1  11675  negfi  12189  deceq1  12742  deceq2  12743  xnegeq  13259  fseq1p1m1  13653  om2uzrdg  14020  uzrdgsuci  14024  seqeq1  14068  seqeq2  14069  seqeq3  14070  seqfeq4  14115  seqof  14123  hashprg  14459  hashtpg  14550  csbwrdg  14609  s1eq  14667  cats1co  14927  s2eqd  14934  s3eqd  14935  s4eqd  14936  s5eqd  14937  s6eqd  14938  s7eqd  14939  s8eqd  14940  xpcogend  15047  shftval  15147  limsupgle  15564  lo1eq  15655  rlimeq  15656  sumeq1  15776  sumeq2w  15779  sumeq2ii  15780  sumeq2sdv  15790  zsum  15804  sumss2  15812  fsumsplitsnun  15841  isumclim3  15845  fsumcom2  15860  incexclem  15925  incexc2  15927  isumshft  15928  prodeq1f  15995  prodeq1  15996  prodeq2w  15999  prodeq2ii  16000  prodeq2sdv  16012  zprod  16026  fprodm1s  16059  fprodp1s  16060  fprodcom2  16073  fprodsplitf  16077  iprodclim3  16089  ef0lem  16166  ruclem7  16326  sadcp1  16547  smupp1  16572  smueqlem  16582  algrp1  16666  dfphi2  16867  prmdiveq  16879  pceulem  16939  vdwlem6  17080  cshwsiun  17193  sloteq  17277  setsid  17301  elbasfv  17309  elbasov  17310  imastset  17610  imasvscaval  17626  isoval  17856  funcoppc  17966  fulloppc  18015  fuccofval  18053  natpropd  18070  catccofval  18195  xpchomfval  18269  xpccofval  18272  lubfval  18438  glbfval  18451  chneq1  18702  chneq2  18703  grpidpropd  18757  gsumpropd2lem  18781  frmdplusg  18962  efmndplusg  18988  grpinvpropd  19137  grpsubpropd  19167  grpsubpropd2  19168  mulgpropd  19238  ecqusaddd  19319  oppgmnd  19480  sylow1lem2  19725  sylow3lem1  19753  prds1  20462  pwsmgp  20466  opprrng  20485  rngidpropd  20555  dvdsrpropd  20556  unitpropd  20557  invrpropd  20558  rhm1  20634  rhmopp  20668  rhmsubclem2  20847  lmhmpropd  21256  lidlrsppropd  21440  rngqiprnglinlem2  21494  lpival  21554  pzriprnglem11  21703  zrhpropd  21726  znle  21748  frlmplusgval  21976  frlmvscafval  21978  ressascl  22110  asclpropd  22111  aspval2  22112  psrbas  22148  psrplusg  22151  psrmulr  22156  psrvscafval  22162  resspsrbas  22187  ressmplbas2  22241  opsrle  22262  opsrbaslem  22264  vr1val  22416  ressply1add  22453  ressply1mul  22454  ressply1vsca  22455  psrplusgpropd  22459  mplbaspropd  22460  psropprmul  22461  ply1baspropd  22466  ply1plusgpropd  22467  ply1sca2  22477  ply1ascl0  22478  ply1ascl1  22479  subrgvr1  22486  coe1mul2lem2  22493  ply1coe1eq  22524  evls1addd  22595  evls1muld  22596  evls1vsca  22597  rhmply1vr1  22608  rhmply1vsca  22609  mamudi  22624  mamudir  22625  matrcl  22633  oftpos  22673  mattpos1  22677  mdetfval  22807  mdetrlin  22823  mdetrsca  22824  mdetrsca2  22825  mdetrlin2  22828  mdetunilem5  22837  madufval  22858  madugsum  22864  idmatidpmat  22961  cpmidpmat  23097  cncmp  23616  2ndcsep  23684  llyeq  23695  nllyeq  23696  xkouni  23824  hmphindis  24022  xkocnv  24039  ptcmplem2  24278  snclseqg  24341  prdstmdd  24349  ustexsym  24441  ucnextcn  24528  metreslem  24587  comet  24738  nrmmetd  24799  nmpropd  24819  isngp3  24823  ngpds  24829  subgnm  24858  tngnm  24876  idnghm  24968  cnmetdval  24995  cnmpopc  25155  htpyco2  25206  phtpyco2  25217  clsocv  25477  rrxprds  25616  rrxnm  25618  rrxplusgvscavalb  25622  ovolunlem1a  25723  voliunlem3  25779  ioombl1lem4  25788  uniioombllem4  25813  itg11  25918  itgeq1f  25998  itgeq1fOLD  25999  itgeq1  26000  itgeq2  26005  iblss2  26033  itgss  26039  itgeqa  26041  itgfsum  26054  itgsplit  26063  ditgeq1  26075  ditgeq2  26076  ditgeq3  26077  dvcmulf  26172  dvmptfsum  26202  dvcnvrelem2  26245  mdegfval  26287  mdegpropd  26309  deg1propd  26311  plyeq0  26436  coe11  26478  dgrlt  26491  dgradd2  26493  dgrmulc  26496  dvply1  26513  fta1lem  26536  pserulm  26653  rlimcnp2  27199  jensenlem1  27219  basellem5  27317  dchrbas  27467  dchrrcl  27472  dchrplusg  27479  dchrfi  27487  lgsdi  27566  lgseisenlem2  27608  lgsquadlem3  27614  dchrmusumlema  27725  rpvmasum2  27744  dchrisum0lema  27746  pntlemg  27830  nosupbnd2lem1  27947  lruneq  28168  addsval  28223  mulsval  28370  seqseq123d  28547  colperpexlem2  29082  symquadmid  29179  tgaaddcpbllem2  29225  axlowdimlem13  29395  uhgrvtxedgiedgb  29577  nb3grprlem1  29824  crctcshlem2  30270  wpthswwlks2on  30416  clwlknf1oclwwlkn  30538  frgrncvvdeq  30773  avril1  30927  0vfval  31071  imsval  31150  imsdval  31151  bcseqi  31585  normpythi  31607  cm0  32074  fh1  32083  pjcji  32149  opsqrlem5  32609  pjsdi2i  32622  pjclem3  32662  pjci  32665  golem1  32736  iuneq12daf  33014  iunrdx  33021  ofresid  33100  cnvprop  33153  coprprop  33156  f1od2  33175  dp2eq1  33303  dp2eq2  33304  fzto1st1  33527  gsumvsca1  33651  gsumvsca2  33652  urpropd  33655  resv1r  33764  nsgqusf1olem2  33828  oppr2idl  33873  opprqus0g  33877  ressply1evls1  33960  esplyfvn  34072  vietalem  34074  lindsunlem  34119  fedgmullem1  34124  fedgmullem2  34125  fedgmul  34126  fldsdrgfldext2  34157  fldextrspunlem1  34170  fldextrspunfld  34171  algextdeglem4  34215  crefeq  34340  rspectopn  34362  xrge0mulc1cn  34436  qqhval2  34477  esumeq12dvaf  34526  esumeq2  34531  esumf1o  34545  esumfzf  34564  esumss  34567  esumpfinvalf  34571  ofceq  34592  carsgclctunlem1  34813  itgeq12dv  34822  ccatmulgnn0dir  35038  breprexpnat  35127  bnj956  35271  bnj1385  35326  bnj96  35359  bnj548  35391  bnj553  35392  bnj554  35393  bnj602  35409  bnj18eq1  35421  bnj1234  35507  bnj1296  35515  bnj1318  35519  bnj1442  35543  bnj1450  35544  cvmliftlem5  35853  cvmliftlem10  35858  cvmlift2lem9  35875  cvmliftphtlem  35881  satfdm  35933  mthmpps  36146  rdgprc  36356  dfrdg2  36357  wsuceq123  36376  wlimeq12  36381  altopthsn  36526  altxpeq1  36538  altxpeq2  36539  nmulprop  36755  ixpeq12dv  36821  prodeq12sdv  36823  itgeq12sdv  36824  ditgeq123dv  36826  cbvcsbdavw  36864  cbvcsbdavw2  36865  cbvrabdavw  36866  cbviundavw  36867  cbviindavw  36868  cbvopab1davw  36869  cbvopab2davw  36870  cbvopabdavw  36871  cbvmptdavw  36872  cbviotadavw  36874  cbvriotadavw  36875  cbvoprab1davw  36876  cbvoprab2davw  36877  cbvoprab3davw  36878  cbvoprab123davw  36879  cbvoprab12davw  36880  cbvoprab23davw  36881  cbvoprab13davw  36882  cbvixpdavw  36883  cbvsumdavw  36884  cbvproddavw  36885  cbvitgdavw  36886  cbvditgdavw  36887  cbvrabdavw2  36890  cbviundavw2  36891  cbviindavw2  36892  cbvmptdavw2  36893  cbvriotadavw2  36895  cbvmpodavw2  36896  cbvmpo1davw2  36897  cbvmpo2davw2  36898  cbvixpdavw2  36899  cbvsumdavw2  36900  cbvproddavw2  36901  cbvitgdavw2  36902  cbvditgdavw2  36903  ee7.2aOLD  37065  ttceq  37092  bj-sngleq  37696  bj-tageq  37705  bj-projeq  37721  bj-projval  37725  bj-1upleq  37728  bj-pr1eq  37731  bj-pr2eq  37745  bj-evaleq  37806  bj-imafv  37988  csbrecsg  38067  csbrdgg  38068  csboprabg  38069  csbmpo123  38070  finxpeq1  38125  finxpeq2  38126  csbfinxpg  38127  finxpreclem4  38133  unceq  38340  unccur  38342  finixpnum  38344  ptrest  38353  poimirlem3  38357  poimirlem9  38363  poimirlem15  38369  poimirlem16  38370  poimirlem26  38380  poimirlem27  38381  mbfposadd  38401  cnambfre  38402  iblabsnclem  38417  ftc1anclem1  38427  heiborlem4  38549  heiborlem6  38551  mpobi123f  38895  iineq12f  38897  mptbi12f  38899  eccnvepres  39019  xrneq1  39129  xrneq2  39132  shiftstableeq2  39216  cosseq  39249  redundss3  39445  riotaclbgBAD  39812  toycom  39831  ldualvbase  39984  ldualfvadd  39986  ldualsca  39990  ldualsbase  39991  ldualsaddN  39992  ldualfvs  39994  ldual0  40005  ldual1  40006  ldualneg  40007  cdleme19f  41166  cdleme20m  41181  cdleme21k  41196  cdleme27b  41226  cdleme31so  41237  cdleme31sn  41238  cdleme31se  41240  cdleme31se2  41241  cdleme31sc  41242  cdleme31sde  41243  cdleme31fv  41248  cdleme40v  41327  cdleme43dN  41350  cdlemeg46ngfr  41376  ltrnco4  41597  tgrpbase  41604  tgrpopr  41605  erngbase  41659  erngfplus  41660  erngfmul  41663  erngbase-rN  41667  erngfplus-rN  41668  erngfmul-rN  41671  dvasca  41864  dvavbase  41871  dvafvadd  41872  dvafvsca  41874  tendocnv  41879  dvhsca  41940  dvhfplusr  41942  dvhvbase  41945  dvhfvadd  41949  dvhfvsca  41958  lcdvadd  42455  lcdsbase  42458  lcdsadd  42459  lcdvs  42461  lcd0  42466  lcd1  42467  lcdneg  42468  fsuppind  43421  imaiinfv  43523  mapfzcons1  43547  rexrabdioph  43620  dnnumch1  43870  dnwech  43874  aomclem6  43885  pwssplit4  43915  pwfi2f1o  43922  mendplusgfval  44007  mendvscafval  44012  harval3  44363  dssmapntrcls  44953  colleq12d  45062  uzmptshftfval  45155  dropab1  45255  dropab2  45256  iineq12dv  45923  rabbida2  45949  rabbida3  45952  itgsinexplem1  46767  wallispi2lem2  46885  fourierdlem36  46956  etransclem4  47051  fcoreslem1  47936  afveq12d  48006  aoveq123d  48051  aovfundmoveq  48054  aovnuoveq  48064  aovvoveq  48065  aovovn0oveq  48067  afv2eq12d  48088  fsumsplitsndif  48254  rngccofvalALTV  49170  rhmsubcALTVlem2  49182  ringccofvalALTV  49204  itscnhlinecirc02plem2  49698  oppfrcl3  50041  oppf1st2nd  50042  uppropd  50092  natoppf  50140  catcrcl  50306  lmdpropd  50568  cmdpropd  50569  lmddu  50578  cmddu  50579  setrecseq  50596  aacllem  50754