Theorem 3eqtr4g 2823

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 2810	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eqtr4di 2816	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 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is used by:  rabbidva2  3418  rabbida4  3441  csbeq1  3856  csbeq2  3858  csbeq2d  3859  csbeq2dv  3860  difeq1  4074  difeq2  4075  uneq2  4116  ineq1  4166  ineq2  4167  symdifeq1  4208  symdifeq2  4209  dfrab3ss  4276  csbprc  4374  csbnestgfw  4387  csbnestgf  4392  disjssun  4428  ifeq1  4491  ifeq2  4492  pweqALT  4577  sneq  4599  csbsng  4674  csbprg  4675  preq1  4699  preq2  4700  tpeq1  4708  tpeq2  4709  tpeq3  4710  prprc1  4731  tpprceq3  4772  opeq1  4838  opeq2  4839  oteq1  4847  oteq2  4848  oteq3  4849  csbopg  4856  uniprg  4888  csbuni  4903  inteq  4915  iineq1  4974  iineq2  4977  iuneq12df  4983  iuneq12d  4986  dfiin2g  4995  iinrab  5033  iinin1  5045  iinxprg  5055  iununi  5065  opabbid  5176  opabbidv  5177  mpteq12da  5194  mpteq12f  5196  mpteq12dva  5197  csbmpt12  5542  xpeq1  5675  xpeq2  5682  rneq  5926  reseq1  5972  reseq2  5973  resima2  6015  resindmOLD  6030  resmpt  6039  resmptf  6041  imaeq1  6057  imaeq2  6058  mptcnv  6138  xpdisj1  6158  xpdisj2  6159  resdisj  6167  dmpropg  6216  rnpropg  6223  cores  6250  cores2  6261  xpco  6290  predeq123  6303  csbpredg  6308  sspred  6311  predres  6340  suceqd  6428  sucprc  6439  iotaeq  6504  iotabi  6505  fntpg  6596  imain  6621  f1oprswap  6866  fveq1  6880  fveq2  6881  fvres  6900  csbfv12  6926  fnimapr  6964  fnimatpd  6965  fvco2  6978  xpprsng  7136  residpr  7139  fsnunfv  7185  fsnunres  7186  funiunfv  7246  f1ofvswap  7304  fliftf  7313  isoini2  7337  eqfunressuc  7359  riotaeqdv  7368  riotabidv  7369  riotauni  7373  riotabidva  7386  snriota  7400  oveq  7416  oveq1  7417  oveq2  7418  oprabbid  7475  oprabbidv  7476  mpoeq123  7482  mpoeq123dva  7484  mpoeq3dva  7487  resmpo  7530  ovres  7576  f1ocnvd  7661  ofeqd  7676  ofreq  7678  fpar  8107  frecseq123  8275  csbfrecsg  8277  wrecseq123  8306  csbwrecsg  8311  onovuni  8325  recseq  8356  tfr2a  8378  rdgeq1  8394  rdgeq2  8395  rdgsucmptf  8411  frsucmpt  8421  seqomeq12  8437  seqomsuc  8440  omopthi  8643  eceq1  8730  eceq2  8732  qseq1  8750  qseq2  8751  uniqs  8767  snecg  8771  ecinxp  8786  qsinxp  8787  erovlem  8807  ecopovtrn  8814  ixpeq1  8902  unfi  9151  supeq1  9401  supeq2  9404  supeq3  9405  supeq123d  9406  infeq1  9433  infeq2  9436  infeq3  9437  infeq123d  9438  infiso  9466  oieq1  9470  oieq2  9471  ordtypelem1  9476  inf3lemc  9591  wemapwe  9662  ttrcleq  9674  r1sucg  9737  r1limg  9739  rankprb  9819  scotteqd  9855  karden  9884  kardenOLD  9885  djueq12  9895  cardiun  9973  acneq  10032  alephlim  10056  alephsuc  10057  alephfplem2  10094  infpssrlem2  10292  fin23lem34  10334  fin23lem35  10335  zorn2lem1  10484  zorn2lem7  10490  fpwwe2lem5  10624  fpwwe2lem12  10631  addpiord  10873  mulpiord  10874  addpqnq  10927  mulpqnq  10930  addassnq  10947  mulassnq  10948  distrnq  10950  lterpq  10959  ltexnq  10964  ltsrpr  11066  00sr  11088  recexsrlem  11092  mulgt0sr  11094  addcnsrec  11132  mulcnsrec  11133  negeq  11453  csbnegg  11458  negsubdi  11518  mulneg1  11654  negfi  12168  deceq1  12720  deceq2  12721  xnegeq  13237  fseq1p1m1  13631  om2uzrdg  13997  uzrdgsuci  14001  seqeq1  14045  seqeq2  14046  seqeq3  14047  seqfeq4  14092  seqof  14100  hashprg  14436  hashtpg  14527  csbwrdg  14586  s1eq  14643  cats1co  14898  s2eqd  14905  s3eqd  14906  s4eqd  14907  s5eqd  14908  s6eqd  14909  s7eqd  14910  s8eqd  14911  xpcogend  15016  shftval  15116  limsupgle  15533  lo1eq  15624  rlimeq  15625  sumeq1  15745  sumeq2w  15748  sumeq2ii  15749  sumeq2sdv  15759  zsum  15774  sumss2  15782  fsumsplitsnun  15811  isumclim3  15815  fsumcom2  15830  incexclem  15895  incexc2  15897  isumshft  15898  prodeq1f  15965  prodeq1  15966  prodeq2w  15969  prodeq2ii  15970  prodeq2sdv  15982  zprod  15996  fprodm1s  16029  fprodp1s  16030  fprodcom2  16043  fprodsplitf  16047  iprodclim3  16059  ef0lem  16136  ruclem7  16296  sadcp1  16517  smupp1  16542  smueqlem  16552  algrp1  16636  dfphi2  16837  prmdiveq  16849  pceulem  16909  vdwlem6  17050  cshwsiun  17163  sloteq  17247  setsid  17271  elbasfv  17279  elbasov  17280  imastset  17580  imasvscaval  17596  isoval  17826  funcoppc  17936  fulloppc  17985  fuccofval  18023  natpropd  18040  catccofval  18165  xpchomfval  18239  xpccofval  18242  lubfval  18408  glbfval  18421  chneq1  18672  chneq2  18673  grpidpropd  18724  gsumpropd2lem  18741  frmdplusg  18917  efmndplusg  18943  grpinvpropd  19085  grpsubpropd  19115  grpsubpropd2  19116  mulgpropd  19186  ecqusaddd  19267  oppgmnd  19428  sylow1lem2  19673  sylow3lem1  19701  prds1  20409  pwsmgp  20413  opprrng  20432  rngidpropd  20502  dvdsrpropd  20503  unitpropd  20504  invrpropd  20505  rhm1  20581  rhmopp  20615  rhmsubclem2  20794  lmhmpropd  21203  lidlrsppropd  21387  rngqiprnglinlem2  21441  lpival  21501  pzriprnglem11  21650  zrhpropd  21673  znle  21695  frlmplusgval  21923  frlmvscafval  21925  ressascl  22055  asclpropd  22056  aspval2  22057  psrbas  22093  psrplusg  22096  psrmulr  22101  psrvscafval  22107  resspsrbas  22132  ressmplbas2  22186  opsrle  22207  opsrbaslem  22209  vr1val  22361  ressply1add  22398  ressply1mul  22399  ressply1vsca  22400  psrplusgpropd  22404  mplbaspropd  22405  psropprmul  22406  ply1baspropd  22411  ply1plusgpropd  22412  ply1sca2  22422  ply1ascl0  22423  ply1ascl1  22424  subrgvr1  22431  coe1mul2lem2  22438  ply1coe1eq  22469  evls1addd  22540  evls1muld  22541  evls1vsca  22542  rhmply1vr1  22553  rhmply1vsca  22554  mamudi  22569  mamudir  22570  matrcl  22578  oftpos  22618  mattpos1  22622  mdetfval  22752  mdetrlin  22768  mdetrsca  22769  mdetrsca2  22770  mdetrlin2  22773  mdetunilem5  22782  madufval  22803  madugsum  22809  idmatidpmat  22903  cpmidpmat  23039  cncmp  23558  2ndcsep  23625  llyeq  23636  nllyeq  23637  xkouni  23765  hmphindis  23963  xkocnv  23980  ptcmplem2  24219  snclseqg  24282  prdstmdd  24290  ustexsym  24382  ucnextcn  24469  metreslem  24528  comet  24679  nrmmetd  24740  nmpropd  24760  isngp3  24764  ngpds  24770  subgnm  24799  tngnm  24817  idnghm  24909  cnmetdval  24936  cnmpopc  25096  htpyco2  25147  phtpyco2  25158  clsocv  25418  rrxprds  25557  rrxnm  25559  rrxplusgvscavalb  25563  ovolunlem1a  25664  voliunlem3  25720  ioombl1lem4  25729  uniioombllem4  25754  itg11  25859  itgeq1f  25939  itgeq1fOLD  25940  itgeq1  25941  itgeq2  25946  iblss2  25974  itgss  25980  itgeqa  25982  itgfsum  25995  itgsplit  26004  ditgeq1  26016  ditgeq2  26017  ditgeq3  26018  dvcmulf  26113  dvmptfsum  26143  dvcnvrelem2  26186  mdegfval  26228  mdegpropd  26250  deg1propd  26252  plyeq0  26377  coe11  26419  dgrlt  26432  dgradd2  26434  dgrmulc  26437  dvply1  26454  fta1lem  26477  pserulm  26594  rlimcnp2  27140  jensenlem1  27160  basellem5  27258  dchrbas  27408  dchrrcl  27413  dchrplusg  27420  dchrfi  27428  lgsdi  27507  lgseisenlem2  27549  lgsquadlem3  27555  dchrmusumlema  27666  rpvmasum2  27685  dchrisum0lema  27687  pntlemg  27771  nosupbnd2lem1  27888  lruneq  28109  addsval  28164  mulsval  28311  seqseq123d  28488  colperpexlem2  29021  symquadmid  29117  axlowdimlem13  29313  uhgrvtxedgiedgb  29495  nb3grprlem1  29739  crctcshlem2  30176  wpthswwlks2on  30322  clwlknf1oclwwlkn  30444  frgrncvvdeq  30669  avril1  30823  0vfval  30967  imsval  31046  imsdval  31047  bcseqi  31481  normpythi  31503  cm0  31970  fh1  31979  pjcji  32045  opsqrlem5  32505  pjsdi2i  32518  pjclem3  32558  pjci  32561  golem1  32632  iuneq12daf  32910  iunrdx  32917  ofresid  32996  cnvprop  33050  coprprop  33053  f1od2  33073  dp2eq1  33201  dp2eq2  33202  fzto1st1  33431  gsumvsca1  33555  gsumvsca2  33556  urpropd  33559  resv1r  33668  nsgqusf1olem2  33732  oppr2idl  33777  opprqus0g  33781  ressply1evls1  33864  esplyfvn  33976  vietalem  33978  lindsunlem  34023  fedgmullem1  34028  fedgmullem2  34029  fedgmul  34030  fldsdrgfldext2  34061  fldextrspunlem1  34074  fldextrspunfld  34075  algextdeglem4  34119  crefeq  34244  rspectopn  34266  xrge0mulc1cn  34340  qqhval2  34381  esumeq12dvaf  34430  esumeq2  34435  esumf1o  34449  esumfzf  34468  esumss  34471  esumpfinvalf  34475  ofceq  34496  carsgclctunlem1  34716  itgeq12dv  34725  ccatmulgnn0dir  34941  breprexpnat  35030  bnj956  35174  bnj1385  35229  bnj96  35262  bnj548  35294  bnj553  35295  bnj554  35296  bnj602  35312  bnj18eq1  35324  bnj1234  35410  bnj1296  35418  bnj1318  35422  bnj1442  35446  bnj1450  35447  cvmliftlem5  35789  cvmliftlem10  35794  cvmlift2lem9  35811  cvmliftphtlem  35817  satfdm  35869  mthmpps  36082  rdgprc  36292  dfrdg2  36293  wsuceq123  36312  wlimeq12  36317  altopthsn  36461  altxpeq1  36473  altxpeq2  36474  nmulprop  36690  ixpeq12dv  36756  prodeq12sdv  36758  itgeq12sdv  36759  ditgeq123dv  36761  cbvcsbdavw  36799  cbvcsbdavw2  36800  cbvrabdavw  36801  cbviundavw  36802  cbviindavw  36803  cbvopab1davw  36804  cbvopab2davw  36805  cbvopabdavw  36806  cbvmptdavw  36807  cbviotadavw  36809  cbvriotadavw  36810  cbvoprab1davw  36811  cbvoprab2davw  36812  cbvoprab3davw  36813  cbvoprab123davw  36814  cbvoprab12davw  36815  cbvoprab23davw  36816  cbvoprab13davw  36817  cbvixpdavw  36818  cbvsumdavw  36819  cbvproddavw  36820  cbvitgdavw  36821  cbvditgdavw  36822  cbvrabdavw2  36825  cbviundavw2  36826  cbviindavw2  36827  cbvmptdavw2  36828  cbvriotadavw2  36830  cbvmpodavw2  36831  cbvmpo1davw2  36832  cbvmpo2davw2  36833  cbvixpdavw2  36834  cbvsumdavw2  36835  cbvproddavw2  36836  cbvitgdavw2  36837  cbvditgdavw2  36838  ee7.2aOLD  37000  ttceq  37027  bj-sngleq  37631  bj-tageq  37640  bj-projeq  37656  bj-projval  37660  bj-1upleq  37663  bj-pr1eq  37666  bj-pr2eq  37680  bj-evaleq  37741  bj-imafv  37923  csbrecsg  38002  csbrdgg  38003  csboprabg  38004  csbmpo123  38005  finxpeq1  38060  finxpeq2  38061  csbfinxpg  38062  finxpreclem4  38068  cureq  38275  unceq  38276  uncov  38280  unccur  38282  finixpnum  38284  ptrest  38298  poimirlem3  38302  poimirlem9  38308  poimirlem15  38314  poimirlem16  38315  poimirlem26  38325  poimirlem27  38326  mbfposadd  38346  cnambfre  38347  iblabsnclem  38362  ftc1anclem1  38372  heiborlem4  38493  heiborlem6  38495  mpobi123f  38839  iineq12f  38841  mptbi12f  38843  eccnvepres  38963  xrneq1  39073  xrneq2  39076  shiftstableeq2  39160  cosseq  39193  redundss3  39389  riotaclbgBAD  39756  toycom  39775  ldualvbase  39928  ldualfvadd  39930  ldualsca  39934  ldualsbase  39935  ldualsaddN  39936  ldualfvs  39938  ldual0  39949  ldual1  39950  ldualneg  39951  cdleme19f  41110  cdleme20m  41125  cdleme21k  41140  cdleme27b  41170  cdleme31so  41181  cdleme31sn  41182  cdleme31se  41184  cdleme31se2  41185  cdleme31sc  41186  cdleme31sde  41187  cdleme31fv  41192  cdleme40v  41271  cdleme43dN  41294  cdlemeg46ngfr  41320  ltrnco4  41541  tgrpbase  41548  tgrpopr  41549  erngbase  41603  erngfplus  41604  erngfmul  41607  erngbase-rN  41611  erngfplus-rN  41612  erngfmul-rN  41615  dvasca  41808  dvavbase  41815  dvafvadd  41816  dvafvsca  41818  tendocnv  41823  dvhsca  41884  dvhfplusr  41886  dvhvbase  41889  dvhfvadd  41893  dvhfvsca  41902  lcdvadd  42399  lcdsbase  42402  lcdsadd  42403  lcdvs  42405  lcd0  42410  lcd1  42411  lcdneg  42412  fsuppind  43350  imaiinfv  43452  mapfzcons1  43476  rexrabdioph  43549  dnnumch1  43799  dnwech  43803  aomclem6  43814  pwssplit4  43844  pwfi2f1o  43851  mendplusgfval  43936  mendvscafval  43941  harval3  44292  dssmapntrcls  44882  colleq12d  44991  uzmptshftfval  45084  dropab1  45184  dropab2  45185  iineq12dv  45852  rabbida2  45878  rabbida3  45881  itgsinexplem1  46696  wallispi2lem2  46814  fourierdlem36  46885  etransclem4  46980  fcoreslem1  47828  afveq12d  47898  aoveq123d  47943  aovfundmoveq  47946  aovnuoveq  47956  aovvoveq  47957  aovovn0oveq  47959  afv2eq12d  47980  fsumsplitsndif  48146  rngccofvalALTV  49063  rhmsubcALTVlem2  49075  ringccofvalALTV  49097  itscnhlinecirc02plem2  49591  oppfrcl3  49936  oppf1st2nd  49937  uppropd  49987  natoppf  50035  catcrcl  50201  lmdpropd  50463  cmdpropd  50464  lmddu  50473  cmddu  50474  setrecseq  50491  aacllem  50649