Theorem 3eqtr4g 2820

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  rabbidva2  3414  rabbida4  3436  csbeq1  3849  csbeq2  3851  csbeq2d  3852  csbeq2dv  3853  difeq1  4056  difeq2  4057  ineq1  4110  ineq2  4111  uneq2  4161  symdifeq1  4200  symdifeq2  4201  dfrab3ss  4268  csbprc  4366  csbnestgfw  4379  csbnestgf  4384  disjssun  4420  ifeq1  4485  ifeq2  4486  pweqALT  4571  sneq  4593  csbsng  4668  csbprg  4669  preq1  4693  preq2  4694  tpeq1  4702  tpeq2  4703  tpeq3  4704  prprc1  4725  tpprceq3  4766  opeq1  4832  opeq2  4833  oteq1  4841  oteq2  4842  oteq3  4843  csbopg  4850  uniprg  4882  csbuni  4897  inteq  4909  iineq1  4968  iineq2  4971  iuneq12df  4977  iuneq12d  4979  dfiin2g  4988  iinrab  5026  iinin1  5038  iinxprg  5048  iununi  5058  opabbid  5169  opabbidv  5170  mpteq12da  5187  mpteq12f  5189  mpteq12dva  5190  csbmpt12  5531  xpeq1  5664  xpeq2  5671  rneq  5917  reseq1  5963  reseq2  5964  resindmOLD  6019  resmpt  6028  resmptf  6030  imaeq1  6046  imaeq2  6047  resima2  6056  dfrn7  6065  mptcnv  6131  xpdisj1  6151  xpdisj2  6152  resdisj  6160  dmpropg  6216  rnpropg  6223  cores  6250  cores2  6261  xpco  6292  predeq123  6305  csbpredg  6310  sspred  6313  predres  6342  suceqd  6430  sucprc  6441  iotaeq  6506  iotabi  6507  fntpg  6600  imain  6625  f1oprswap  6870  fveq1  6884  fveq2  6885  fvres  6904  csbfv12  6930  fnimapr  6968  fnimatpd  6969  fvco2  6982  xpprsng  7142  xpsnprg  7143  xpsntpg  7144  residpr  7146  fsnunfv  7192  fsnunres  7193  funiunfv  7252  f1ofvswap  7314  fliftf  7323  isoini2  7347  eqfunressuc  7371  riotaeqdv  7378  riotabidv  7379  riotauni  7383  riotabidva  7396  snriota  7410  oveq  7426  oveq1  7427  oveq2  7428  oprabbid  7485  oprabbidv  7486  mpoeq123  7492  mpoeq123dva  7494  mpoeq3dva  7497  resmpo  7540  ovres  7586  f1ocnvd  7672  mpt3eqdv  7686  ofeqd  7695  ofreq  7697  fpar  8127  frecseq123  8300  csbfrecsg  8302  wrecseq123  8331  csbwrecsg  8336  onovuni  8350  recseq  8381  tfr2a  8403  rdgeq1  8419  rdgeq2  8420  rdgsucmptf  8436  frsucmpt  8446  seqomeq12  8464  seqomsuc  8467  omopthi  8670  eceq1  8757  eceq2  8759  qseq1  8777  qseq2  8778  uniqs  8794  snecg  8798  ecinxp  8813  qsinxp  8814  erovlem  8834  ecopovtrn  8841  cureq  8889  uncov  8893  ixpeq1  8936  unfi  9186  supeq1  9437  supeq2  9440  supeq3  9441  supeq123d  9442  infeq1  9469  infeq2  9472  infeq3  9473  infeq123d  9474  infiso  9502  oieq1  9506  oieq2  9507  ordtypelem1  9512  inf3lemc  9627  wemapwe  9698  ttrcleq  9710  r1sucg  9776  r1limg  9778  rankprb  9865  scotteqd  9930  karden  9959  kardenOLD  9960  djueq12  9985  cardiun  10063  acneq  10122  alephlim  10146  alephsuc  10147  alephfplem2  10184  infpssrlem2  10382  fin23lem34  10424  fin23lem35  10425  zorn2lem1  10574  zorn2lem7  10580  fpwwe2lem5  10720  fpwwe2lem12  10727  addpiord  10969  mulpiord  10970  addpqnq  11023  mulpqnq  11026  addassnq  11043  mulassnq  11044  distrnq  11046  lterpq  11055  ltexnq  11060  ltsrpr  11162  00sr  11184  recexsrlem  11188  mulgt0sr  11190  addcnsrec  11228  mulcnsrec  11229  negeq  11549  csbnegg  11554  negsubdi  11614  mulneg1  11752  negfi  12266  deceq1  12819  deceq2  12820  xnegeq  13337  fseq1p1m1  13732  om2uzrdg  14099  uzrdgsuci  14103  seqeq1  14147  seqeq2  14148  seqeq3  14149  seqfeq4  14194  seqof  14202  hashprg  14539  hashtpg  14630  csbwrdg  14689  s1eq  14747  cats1co  15007  s2eqd  15014  s3eqd  15015  s4eqd  15016  s5eqd  15017  s6eqd  15018  s7eqd  15019  s8eqd  15020  xpcogend  15127  shftval  15227  limsupgle  15644  lo1eq  15735  rlimeq  15736  sumeq1  15856  sumeq2w  15859  sumeq2ii  15860  sumeq2sdv  15870  zsum  15884  sumss2  15892  fsumsplitsnun  15921  isumclim3  15925  fsumcom2  15940  incexclem  16005  incexc2  16007  isumshft  16008  prodeq1f  16075  prodeq1  16076  prodeq2w  16079  prodeq2ii  16080  prodeq2sdv  16091  zprod  16104  fprodm1s  16137  fprodp1s  16138  fprodcom2  16151  fprodsplitf  16155  iprodclim3  16167  ef0lem  16244  ruclem7  16404  sadcp1  16625  smupp1  16650  smueqlem  16660  algrp1  16749  dfphi2  16951  prmdiveq  16963  pceulem  17023  vdwlem6  17164  cshwsiun  17277  sloteq  17361  setsid  17385  elbasfv  17393  elbasov  17394  imastset  17694  imasvscaval  17710  isoval  17940  funcoppc  18050  fulloppc  18099  fuccofval  18137  natpropd  18154  catccofval  18279  xpchomfval  18353  xpccofval  18356  lubfval  18522  glbfval  18535  chneq1  18786  chneq2  18787  grpidpropd  18842  gsumpropd2lem  18868  frmdplusg  19050  efmndplusg  19076  grpinvpropd  19225  grpsubpropd  19255  grpsubpropd2  19256  mulgpropd  19326  ecqusaddd  19407  oppgmnd  19568  sylow1lem2  19813  sylow3lem1  19841  prds1  20552  pwsmgp  20556  opprrng  20575  rngidpropd  20645  dvdsrpropd  20646  unitpropd  20647  invrpropd  20648  rhm1  20724  rhmopp  20759  rhmsubclem2  20938  lmhmpropd  21348  lidlrsppropd  21532  rngqiprnglinlem2  21588  lpival  21648  pzriprnglem11  21797  zrhpropd  21820  znle  21842  frlmplusgval  22070  frlmvscafval  22072  ressascl  22204  asclpropd  22205  aspval2  22206  psrbas  22242  psrplusg  22245  psrmulr  22250  psrvscafval  22256  resspsrbas  22281  ressmplbas2  22335  opsrle  22356  opsrbaslem  22358  vr1val  22510  ressply1add  22547  ressply1mul  22548  ressply1vsca  22549  psrplusgpropd  22553  mplbaspropd  22554  psropprmul  22555  ply1baspropd  22560  ply1plusgpropd  22561  ply1sca2  22571  ply1ascl0  22572  ply1ascl1  22573  subrgvr1  22580  coe1mul2lem2  22587  ply1coe1eq  22618  evls1addd  22689  evls1muld  22690  evls1vsca  22691  rhmply1vr1  22702  rhmply1vsca  22703  mamudi  22718  mamudir  22719  matrcl  22727  oftpos  22767  mattpos1  22771  mdetfval  22901  mdetrlin  22917  mdetrsca  22918  mdetrsca2  22919  mdetrlin2  22922  mdetunilem5  22931  madufval  22952  madugsum  22958  idmatidpmat  23055  cpmidpmat  23191  cncmp  23710  2ndcsep  23778  llyeq  23789  nllyeq  23790  xkouni  23918  hmphindis  24116  xkocnv  24133  ptcmplem2  24372  snclseqg  24435  prdstmdd  24443  ustexsym  24535  ucnextcn  24622  metreslem  24681  comet  24832  nrmmetd  24893  nmpropd  24913  isngp3  24917  ngpds  24923  subgnm  24952  tngnm  24970  idnghm  25062  cnmetdval  25089  cnmpopc  25249  htpyco2  25300  phtpyco2  25311  clsocv  25571  rrxprds  25710  rrxnm  25712  rrxplusgvscavalb  25716  ovolunlem1a  25817  voliunlem3  25873  ioombl1lem4  25882  uniioombllem4  25907  itg11  26012  itgeq1f  26092  itgeq1  26093  itgeq2  26098  iblss2  26126  itgss  26132  itgeqa  26134  itgfsum  26147  itgsplit  26156  ditgeq1  26168  ditgeq2  26169  ditgeq3  26170  dvcmulf  26265  dvmptfsum  26295  dvcnvrelem2  26338  mdegfval  26380  mdegpropd  26402  deg1propd  26404  plyeq0  26530  coe11  26572  dgrlt  26585  dgradd2  26587  dgrmulc  26590  dvply1  26605  fta1lem  26628  pserulm  26749  rlimcnp2  27294  jensenlem1  27314  basellem5  27412  dchrbas  27562  dchrrcl  27567  dchrplusg  27574  dchrfi  27582  lgsdi  27661  lgseisenlem2  27703  lgsquadlem3  27709  dchrmusumlema  27820  rpvmasum2  27839  dchrisum0lema  27841  pntlemg  27925  nosupbnd2lem1  28072  lruneq  28293  addsval  28348  mulsval  28495  seqseq123d  28672  colperpexlem2  29207  symquadmid  29304  tgaaddcpbllem2  29350  axlowdimlem13  29532  uhgrvtxedgiedgb  29714  nb3grprlem1  29961  crctcshlem2  30407  wpthswwlks2on  30553  clwlknf1oclwwlkn  30675  frgrncvvdeq  30910  avril1  31064  0vfval  31208  imsval  31287  imsdval  31288  bcseqi  31722  normpythi  31744  cm0  32211  fh1  32220  pjcji  32286  opsqrlem5  32746  pjsdi2i  32759  pjclem3  32799  pjci  32802  golem1  32873  iuneq12daf  33193  iunrdx  33200  ofresid  33278  cnvprop  33331  coprprop  33334  f1od2  33353  dp2eq1  33481  dp2eq2  33482  fzto1st1  33705  gsumvsca1  33829  gsumvsca2  33830  urpropd  33833  resv1r  33942  nsgqusf1olem2  34007  oppr2idl  34052  opprqus0g  34056  ressply1evls1  34139  esplyfvn  34251  vietalem  34253  lindsunlem  34298  fedgmullem1  34303  fedgmullem2  34304  fedgmul  34305  fldsdrgfldext2  34336  fldextrspunlem1  34349  fldextrspunfld  34350  algextdeglem4  34394  crefeq  34519  rspectopn  34541  xrge0mulc1cn  34615  qqhval2  34656  esumeq12dvaf  34705  esumeq2  34710  esumf1o  34724  esumfzf  34743  esumss  34746  esumpfinvalf  34750  ofceq  34771  carsgclctunlem1  34991  itgeq12dv  35000  ccatmulgnn0dir  35216  breprexpnat  35305  bnj956  35449  bnj1385  35504  bnj96  35537  bnj548  35569  bnj553  35570  bnj554  35571  bnj602  35587  bnj18eq1  35599  bnj1234  35685  bnj1296  35693  bnj1318  35697  bnj1442  35721  bnj1450  35722  cvmliftlem5  36096  cvmliftlem10  36101  cvmlift2lem9  36118  cvmliftphtlem  36124  satfdm  36176  mthmpps  36389  rdgprc  36598  dfrdg2  36599  wsuceq123  36618  wlimeq12  36623  altopthsn  36768  altxpeq1  36780  altxpeq2  36781  nmulprop  36981  ixpeq12dv  37047  prodeq12sdv  37049  itgeq12sdv  37050  ditgeq123dv  37052  cbvcsbdavw  37090  cbvcsbdavw2  37091  cbvrabdavw  37092  cbviundavw  37093  cbviindavw  37094  cbvopab1davw  37095  cbvopab2davw  37096  cbvopabdavw  37097  cbvmptdavw  37098  cbviotadavw  37100  cbvriotadavw  37101  cbvoprab1davw  37102  cbvoprab2davw  37103  cbvoprab3davw  37104  cbvoprab123davw  37105  cbvoprab12davw  37106  cbvoprab23davw  37107  cbvoprab13davw  37108  cbvixpdavw  37109  cbvsumdavw  37110  cbvproddavw  37111  cbvitgdavw  37112  cbvditgdavw  37113  cbvrabdavw2  37116  cbviundavw2  37117  cbviindavw2  37118  cbvmptdavw2  37119  cbvriotadavw2  37121  cbvmpodavw2  37122  cbvmpo1davw2  37123  cbvmpo2davw2  37124  cbvixpdavw2  37125  cbvsumdavw2  37126  cbvproddavw2  37127  cbvitgdavw2  37128  cbvditgdavw2  37129  ee7.2aOLD  37291  ttceq  37318  bj-sngleq  37922  bj-tageq  37931  bj-projeq  37947  bj-projval  37951  bj-1upleq  37954  bj-pr1eq  37957  bj-pr2eq  37971  bj-evaleq  38034  bj-imafv  38215  csbrecsg  38294  csbrdgg  38295  csboprabg  38296  csbmpo123  38297  finxpeq1  38352  finxpeq2  38353  csbfinxpg  38354  finxpreclem4  38360  unceq  38567  unccur  38569  finixpnum  38571  ptrest  38580  poimirlem3  38584  poimirlem9  38590  poimirlem15  38596  poimirlem16  38597  poimirlem26  38607  poimirlem27  38608  mbfposadd  38628  cnambfre  38629  iblabsnclem  38644  ftc1anclem1  38654  heiborlem4  38791  heiborlem6  38793  mpobi123f  39137  iineq12f  39139  mptbi12f  39141  eccnvepres  39261  xrneq1  39371  xrneq2  39374  shiftstableeq2  39458  cosseq  39491  redundss3  39687  riotaclbgBAD  40054  toycom  40073  ldualvbase  40226  ldualfvadd  40228  ldualsca  40232  ldualsbase  40233  ldualsaddN  40234  ldualfvs  40236  ldual0  40247  ldual1  40248  ldualneg  40249  cdleme19f  41408  cdleme20m  41423  cdleme21k  41438  cdleme27b  41468  cdleme31so  41479  cdleme31sn  41480  cdleme31se  41482  cdleme31se2  41483  cdleme31sc  41484  cdleme31sde  41485  cdleme31fv  41490  cdleme40v  41569  cdleme43dN  41592  cdlemeg46ngfr  41618  ltrnco4  41839  tgrpbase  41846  tgrpopr  41847  erngbase  41901  erngfplus  41902  erngfmul  41905  erngbase-rN  41909  erngfplus-rN  41910  erngfmul-rN  41913  dvasca  42106  dvavbase  42113  dvafvadd  42114  dvafvsca  42116  tendocnv  42121  dvhsca  42182  dvhfplusr  42184  dvhvbase  42187  dvhfvadd  42191  dvhfvsca  42200  lcdvadd  42697  lcdsbase  42700  lcdsadd  42701  lcdvs  42703  lcd0  42708  lcd1  42709  lcdneg  42710  fsuppind  43661  imaiinfv  43746  mapfzcons1  43770  rexrabdioph  43843  dnnumch1  44093  dnwech  44097  aomclem6  44103  pwssplit4  44133  pwfi2f1o  44140  mendplusgfval  44225  mendvscafval  44230  harval3  44581  dssmapntrcls  45170  colleq12d  45279  uzmptshftfval  45372  dropab1  45472  dropab2  45473  iineq12dv  46163  rabbida2  46189  rabbida3  46192  itgsinexplem1  47006  wallispi2lem2  47124  fourierdlem36  47195  etransclem4  47290  fcoreslem1  48175  afveq12d  48245  aoveq123d  48290  aovfundmoveq  48293  aovnuoveq  48303  aovvoveq  48304  aovovn0oveq  48306  afv2eq12d  48327  fsumsplitsndif  48493  rngccofvalALTV  49409  rhmsubcALTVlem2  49421  ringccofvalALTV  49443  itscnhlinecirc02plem2  49937  oppfrcl3  50280  oppf1st2nd  50281  uppropd  50331  natoppf  50379  catcrcl  50545  lmdpropd  50807  cmdpropd  50808  lmddu  50817  cmddu  50818  setrecseq  50830  aacllem  50981