Theorem 3eqtr4g 2797

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

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

This theorem is referenced by:  rabbidva2  3403  rabbida4  3426  rabeqf  3435  csbeq1  3854  csbeq2  3856  csbeq2d  3857  csbeq2dv  3858  difeq1  4073  difeq2  4074  uneq2  4116  ineq1  4167  ineq2  4168  symdifeq1  4209  symdifeq2  4210  dfrab3ss  4277  csbprc  4363  csbnestgfw  4376  csbnestgf  4381  disjssun  4422  ifeq1  4485  ifeq2  4486  pweqALT  4571  sneq  4592  rabsneq  4601  csbsng  4667  csbprg  4668  preq1  4692  preq2  4693  tpeq1  4701  tpeq2  4702  tpeq3  4703  prprc1  4724  tpprceq3  4762  opeq1  4831  opeq2  4832  oteq1  4840  oteq2  4841  oteq3  4842  csbopg  4849  uniprg  4881  csbuni  4895  inteq  4907  iineq1  4966  iineq2  4969  iuneq12df  4975  iuneq12d  4978  dfiin2g  4988  iinrab  5026  iinin1  5036  iinxprg  5046  iununi  5056  opabbid  5165  opabbidv  5166  mpteq12da  5183  mpteq12f  5185  mpteq12dva  5186  csbmpt12  5515  xpeq1  5648  xpeq2  5655  rneq  5895  reseq1  5942  reseq2  5943  resima2  5985  resindm  5999  resmpt  6006  resmptf  6008  imaeq1  6024  imaeq2  6025  mptcnv  6106  xpdisj1  6129  xpdisj2  6130  resdisj  6137  dmpropg  6183  rnpropg  6190  cores  6217  cores2  6228  xpco  6257  predeq123  6270  csbpredg  6275  sspred  6278  predres  6307  suceqd  6394  sucprc  6405  iotaeq  6470  iotabi  6471  fntpg  6562  imain  6587  f1oprswap  6829  fveq1  6843  fveq2  6844  fvres  6863  csbfv12  6889  fnimapr  6927  fnimatpd  6928  fvco2  6941  xpprsng  7097  residpr  7100  fsnunfv  7145  fsnunres  7146  funiunfv  7206  f1ofvswap  7264  fliftf  7273  isoini2  7297  eqfunressuc  7319  riotaeqdv  7328  riotabidv  7329  riotauni  7333  riotabidva  7346  snriota  7360  oveq  7376  oveq1  7377  oveq2  7378  oprabbid  7435  oprabbidv  7436  mpoeq123  7442  mpoeq123dva  7444  mpoeq3dva  7447  resmpo  7490  ovres  7536  f1ocnvd  7621  ofeqd  7636  ofreq  7638  fpar  8070  frecseq123  8236  csbfrecsg  8238  wrecseq123  8267  csbwrecsg  8272  onovuni  8286  recseq  8317  tfr2a  8338  rdgeq1  8354  rdgeq2  8355  rdgsucmptf  8371  frsucmpt  8381  seqomeq12  8397  seqomsuc  8400  omopthi  8601  eceq1  8687  eceq2  8689  qseq1  8707  qseq2  8708  uniqs  8724  snecg  8728  ecinxp  8743  qsinxp  8744  erovlem  8764  ecopovtrn  8771  ixpeq1  8860  unfi  9109  supeq1  9362  supeq2  9365  supeq3  9366  supeq123d  9367  infeq1  9394  infeq2  9397  infeq3  9398  infeq123d  9399  infiso  9427  oieq1  9431  oieq2  9432  ordtypelem1  9437  inf3lemc  9549  wemapwe  9620  ttrcleq  9632  r1sucg  9695  r1limg  9697  rankprb  9777  karden  9821  djueq12  9830  cardiun  9908  acneq  9967  alephlim  9991  alephsuc  9992  alephfplem2  10029  infpssrlem2  10228  fin23lem34  10270  fin23lem35  10271  zorn2lem1  10420  zorn2lem7  10426  fpwwe2lem5  10560  fpwwe2lem12  10567  addpiord  10809  mulpiord  10810  addpqnq  10863  mulpqnq  10866  addassnq  10883  mulassnq  10884  distrnq  10886  lterpq  10895  ltexnq  10900  ltsrpr  11002  00sr  11024  recexsrlem  11028  mulgt0sr  11030  addcnsrec  11068  mulcnsrec  11069  negeq  11386  csbnegg  11391  negsubdi  11451  mulneg1  11587  negfi  12105  deceq1  12626  deceq2  12627  xnegeq  13136  fseq1p1m1  13528  om2uzrdg  13893  uzrdgsuci  13897  seqeq1  13941  seqeq2  13942  seqeq3  13943  seqfeq4  13988  seqof  13996  hashprg  14332  hashtpg  14422  csbwrdg  14481  s1eq  14538  cats1co  14793  s2eqd  14800  s3eqd  14801  s4eqd  14802  s5eqd  14803  s6eqd  14804  s7eqd  14805  s8eqd  14806  xpcogend  14911  shftval  15011  limsupgle  15414  lo1eq  15505  rlimeq  15506  sumeq1  15626  sumeq2w  15629  sumeq2ii  15630  sumeq2sdv  15640  zsum  15655  sumss2  15663  fsumsplitsnun  15692  isumclim3  15696  fsumcom2  15711  incexclem  15773  incexc2  15775  isumshft  15776  prodeq1f  15843  prodeq1  15844  prodeq2w  15847  prodeq2ii  15848  prodeq2sdv  15860  zprod  15874  fprodm1s  15907  fprodp1s  15908  fprodcom2  15921  fprodsplitf  15925  iprodclim3  15937  ef0lem  16015  ruclem7  16175  sadcp1  16396  smupp1  16421  smueqlem  16431  algrp1  16515  dfphi2  16715  prmdiveq  16727  pceulem  16787  vdwlem6  16928  cshwsiun  17041  sloteq  17124  setsid  17148  elbasfv  17156  elbasov  17157  imastset  17457  imasvscaval  17473  isoval  17703  funcoppc  17813  fulloppc  17862  fuccofval  17900  natpropd  17917  catccofval  18042  xpchomfval  18116  xpccofval  18119  lubfval  18285  glbfval  18298  chneq1  18549  chneq2  18550  grpidpropd  18601  gsumpropd2lem  18618  frmdplusg  18793  efmndplusg  18819  grpinvpropd  18962  grpsubpropd  18992  grpsubpropd2  18993  mulgpropd  19063  ecqusaddd  19138  oppgmnd  19300  sylow1lem2  19545  sylow3lem1  19573  prds1  20275  pwsmgp  20279  opprrng  20298  rngidpropd  20368  dvdsrpropd  20369  unitpropd  20370  invrpropd  20371  rhm1  20441  rhmopp  20459  rhmsubclem2  20636  lmhmpropd  21042  lidlrsppropd  21216  rngqiprnglinlem2  21264  lpival  21296  pzriprnglem11  21463  zrhpropd  21486  znle  21508  frlmplusgval  21736  frlmvscafval  21738  ressascl  21869  asclpropd  21870  aspval2  21871  psrbas  21906  psrplusg  21909  psrmulr  21915  psrvscafval  21921  resspsrbas  21946  ressmplbas2  21999  opsrle  22019  opsrbaslem  22021  vr1val  22149  ressply1add  22187  ressply1mul  22188  ressply1vsca  22189  psrplusgpropd  22193  mplbaspropd  22194  psropprmul  22195  ply1baspropd  22200  ply1plusgpropd  22201  ply1sca2  22211  ply1ascl0  22212  ply1ascl1  22213  subrgvr1  22220  coe1mul2lem2  22227  ply1coe1eq  22261  evls1addd  22332  evls1muld  22333  evls1vsca  22334  rhmply1vr1  22348  rhmply1vsca  22349  mamudi  22364  mamudir  22365  matrcl  22373  oftpos  22413  mattpos1  22417  mdetfval  22547  mdetrlin  22563  mdetrsca  22564  mdetrsca2  22565  mdetrlin2  22568  mdetunilem5  22577  madufval  22598  madugsum  22604  idmatidpmat  22698  cpmidpmat  22834  cncmp  23353  2ndcsep  23420  llyeq  23431  nllyeq  23432  xkouni  23560  hmphindis  23758  xkocnv  23775  ptcmplem2  24014  snclseqg  24077  prdstmdd  24085  ustexsym  24177  ucnextcn  24264  metreslem  24323  comet  24474  nrmmetd  24535  nmpropd  24555  isngp3  24559  ngpds  24565  subgnm  24594  tngnm  24612  idnghm  24704  cnmetdval  24731  cnmpopc  24895  htpyco2  24951  phtpyco2  24962  clsocv  25223  rrxprds  25362  rrxnm  25364  rrxplusgvscavalb  25368  ovolunlem1a  25470  voliunlem3  25526  ioombl1lem4  25535  uniioombllem4  25560  itg11  25665  itgeq1f  25745  itgeq1fOLD  25746  itgeq1  25747  itgeq2  25752  iblss2  25780  itgss  25786  itgeqa  25788  itgfsum  25801  itgsplit  25810  ditgeq1  25822  ditgeq2  25823  ditgeq3  25824  dvcmulf  25921  dvmptfsum  25952  dvcnvrelem2  25996  mdegfval  26040  mdegpropd  26062  deg1propd  26064  plyeq0  26189  coe11  26231  dgrlt  26245  dgradd2  26247  dgrmulc  26250  dvply1  26264  fta1lem  26288  pserulm  26404  rlimcnp2  26949  jensenlem1  26970  basellem5  27068  dchrbas  27219  dchrrcl  27224  dchrplusg  27231  dchrfi  27239  lgsdi  27318  lgseisenlem2  27360  lgsquadlem3  27366  dchrmusumlema  27477  rpvmasum2  27496  dchrisum0lema  27498  pntlemg  27582  nosupbnd2lem1  27700  lruneq  27920  addsval  27975  mulsval  28122  seqseq123d  28299  colperpexlem2  28821  axlowdimlem13  29045  uhgrvtxedgiedgb  29227  nb3grprlem1  29471  crctcshlem2  29909  wpthswwlks2on  30055  clwlknf1oclwwlkn  30177  frgrncvvdeq  30402  avril1  30556  0vfval  30700  imsval  30779  imsdval  30780  bcseqi  31214  normpythi  31236  cm0  31703  fh1  31712  pjcji  31778  opsqrlem5  32238  pjsdi2i  32251  pjclem3  32291  pjci  32294  golem1  32365  iuneq12daf  32649  iunrdx  32656  ofresid  32738  cnvprop  32792  coprprop  32795  f1od2  32815  dp2eq1  32971  dp2eq2  32972  fzto1st1  33202  gsumvsca1  33326  gsumvsca2  33327  urpropd  33331  resv1r  33438  nsgqusf1olem2  33513  oppr2idl  33585  opprqus0g  33589  ressply1evls1  33664  esplyfvn  33760  vietalem  33762  lindsunlem  33808  fedgmullem1  33813  fedgmullem2  33814  fedgmul  33815  fldsdrgfldext2  33846  fldextrspunlem1  33859  fldextrspunfld  33860  algextdeglem4  33904  crefeq  34029  rspectopn  34051  xrge0mulc1cn  34125  qqhval2  34166  esumeq12dvaf  34215  esumeq2  34220  esumf1o  34234  esumfzf  34253  esumss  34256  esumpfinvalf  34260  ofceq  34281  carsgclctunlem1  34501  itgeq12dv  34510  ccatmulgnn0dir  34726  breprexpnat  34818  bnj956  34959  bnj1385  35014  bnj96  35047  bnj548  35079  bnj553  35080  bnj554  35081  bnj602  35097  bnj18eq1  35109  bnj1234  35195  bnj1296  35203  bnj1318  35207  bnj1442  35231  bnj1450  35232  cvmliftlem5  35511  cvmliftlem10  35516  cvmlift2lem9  35533  cvmliftphtlem  35539  satfdm  35591  mthmpps  35804  rdgprc  36014  dfrdg2  36015  wsuceq123  36034  wlimeq12  36039  altopthsn  36183  altxpeq1  36195  altxpeq2  36196  ixpeq12dv  36438  prodeq12sdv  36440  itgeq12sdv  36441  ditgeq123dv  36443  cbvcsbdavw  36481  cbvcsbdavw2  36482  cbvrabdavw  36483  cbviundavw  36484  cbviindavw  36485  cbvopab1davw  36486  cbvopab2davw  36487  cbvopabdavw  36488  cbvmptdavw  36489  cbviotadavw  36491  cbvriotadavw  36492  cbvoprab1davw  36493  cbvoprab2davw  36494  cbvoprab3davw  36495  cbvoprab123davw  36496  cbvoprab12davw  36497  cbvoprab23davw  36498  cbvoprab13davw  36499  cbvixpdavw  36500  cbvsumdavw  36501  cbvproddavw  36502  cbvitgdavw  36503  cbvditgdavw  36504  cbvrabdavw2  36507  cbviundavw2  36508  cbviindavw2  36509  cbvmptdavw2  36510  cbvriotadavw2  36512  cbvmpodavw2  36513  cbvmpo1davw2  36514  cbvmpo2davw2  36515  cbvixpdavw2  36516  cbvsumdavw2  36517  cbvproddavw2  36518  cbvitgdavw2  36519  cbvditgdavw2  36520  ee7.2aOLD  36683  bj-sngleq  37242  bj-tageq  37251  bj-projeq  37267  bj-projval  37271  bj-1upleq  37274  bj-pr1eq  37277  bj-pr2eq  37291  bj-evaleq  37351  bj-imafv  37533  csbrecsg  37610  csbrdgg  37611  csboprabg  37612  csbmpo123  37613  finxpeq1  37668  finxpeq2  37669  csbfinxpg  37670  finxpreclem4  37676  cureq  37876  unceq  37877  uncov  37881  unccur  37883  finixpnum  37885  ptrest  37899  poimirlem3  37903  poimirlem9  37909  poimirlem15  37915  poimirlem16  37916  poimirlem26  37926  poimirlem27  37927  mbfposadd  37947  cnambfre  37948  iblabsnclem  37963  ftc1anclem1  37973  heiborlem4  38094  heiborlem6  38096  mpobi123f  38442  iineq12f  38444  mptbi12f  38446  eccnvepres  38566  xrneq1  38676  xrneq2  38679  shiftstableeq2  38763  cosseq  38796  redundss3  38992  riotaclbgBAD  39359  toycom  39378  ldualvbase  39531  ldualfvadd  39533  ldualsca  39537  ldualsbase  39538  ldualsaddN  39539  ldualfvs  39541  ldual0  39552  ldual1  39553  ldualneg  39554  cdleme19f  40713  cdleme20m  40728  cdleme21k  40743  cdleme27b  40773  cdleme31so  40784  cdleme31sn  40785  cdleme31se  40787  cdleme31se2  40788  cdleme31sc  40789  cdleme31sde  40790  cdleme31fv  40795  cdleme40v  40874  cdleme43dN  40897  cdlemeg46ngfr  40923  ltrnco4  41144  tgrpbase  41151  tgrpopr  41152  erngbase  41206  erngfplus  41207  erngfmul  41210  erngbase-rN  41214  erngfplus-rN  41215  erngfmul-rN  41218  dvasca  41411  dvavbase  41418  dvafvadd  41419  dvafvsca  41421  tendocnv  41426  dvhsca  41487  dvhfplusr  41489  dvhvbase  41492  dvhfvadd  41496  dvhfvsca  41505  lcdvadd  42002  lcdsbase  42005  lcdsadd  42006  lcdvs  42008  lcd0  42013  lcd1  42014  lcdneg  42015  fsuppind  42977  imaiinfv  43079  mapfzcons1  43103  rexrabdioph  43180  dnnumch1  43430  dnwech  43434  aomclem6  43445  pwssplit4  43475  pwfi2f1o  43482  mendplusgfval  43567  mendvscafval  43572  harval3  43923  dssmapntrcls  44513  scotteqd  44622  colleq12d  44638  uzmptshftfval  44731  dropab1  44831  dropab2  44832  iineq12dv  45494  rabbida2  45520  rabbida3  45523  itgsinexplem1  46341  wallispi2lem2  46459  fourierdlem36  46530  etransclem4  46625  fcoreslem1  47452  afveq12d  47522  aoveq123d  47567  aovfundmoveq  47570  aovnuoveq  47580  aovvoveq  47581  aovovn0oveq  47583  afv2eq12d  47604  fsumsplitsndif  47762  rngccofvalALTV  48659  rhmsubcALTVlem2  48671  ringccofvalALTV  48693  itscnhlinecirc02plem2  49172  oppfrcl3  49518  oppf1st2nd  49519  uppropd  49569  natoppf  49617  catcrcl  49783  lmdpropd  50045  cmdpropd  50046  lmddu  50055  cmddu  50056  setrecseq  50073  aacllem  50189