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 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 2732

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

This theorem is used by:  rabbidva2  3414  rabbida4  3436  csbeq1  3850  csbeq2  3852  csbeq2d  3853  csbeq2dv  3854  difeq1  4067  difeq2  4068  uneq2  4109  ineq1  4159  ineq2  4160  symdifeq1  4201  symdifeq2  4202  dfrab3ss  4269  csbprc  4367  csbnestgfw  4380  csbnestgf  4385  disjssun  4421  ifeq1  4486  ifeq2  4487  pweqALT  4572  sneq  4594  csbsng  4669  csbprg  4670  preq1  4694  preq2  4695  tpeq1  4703  tpeq2  4704  tpeq3  4705  prprc1  4726  tpprceq3  4767  opeq1  4833  opeq2  4834  oteq1  4842  oteq2  4843  oteq3  4844  csbopg  4851  uniprg  4883  csbuni  4898  inteq  4910  iineq1  4969  iineq2  4972  iuneq12df  4978  iuneq12d  4980  dfiin2g  4989  iinrab  5027  iinin1  5039  iinxprg  5049  iununi  5059  opabbid  5170  opabbidv  5171  mpteq12da  5188  mpteq12f  5190  mpteq12dva  5191  csbmpt12  5536  xpeq1  5669  xpeq2  5676  rneq  5922  reseq1  5968  reseq2  5969  resima2  6011  resindmOLD  6026  resmpt  6035  resmptf  6037  imaeq1  6053  imaeq2  6054  mptcnv  6134  xpdisj1  6155  xpdisj2  6156  resdisj  6164  dmpropg  6213  rnpropg  6220  cores  6247  cores2  6258  xpco  6289  predeq123  6302  csbpredg  6307  sspred  6310  predres  6339  suceqd  6427  sucprc  6438  iotaeq  6503  iotabi  6504  fntpg  6596  imain  6621  f1oprswap  6866  fveq1  6880  fveq2  6881  fvres  6900  csbfv12  6926  fnimapr  6964  fnimatpd  6965  fvco2  6978  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  7686  ofreq  7688  fpar  8118  frecseq123  8286  csbfrecsg  8288  wrecseq123  8317  csbwrecsg  8322  onovuni  8336  recseq  8367  tfr2a  8389  rdgeq1  8405  rdgeq2  8406  rdgsucmptf  8422  frsucmpt  8432  seqomeq12  8450  seqomsuc  8453  omopthi  8656  eceq1  8743  eceq2  8745  qseq1  8763  qseq2  8764  uniqs  8780  snecg  8784  ecinxp  8799  qsinxp  8800  erovlem  8820  ecopovtrn  8827  cureq  8875  uncov  8879  ixpeq1  8922  unfi  9172  supeq1  9422  supeq2  9425  supeq3  9426  supeq123d  9427  infeq1  9454  infeq2  9457  infeq3  9458  infeq123d  9459  infiso  9487  oieq1  9491  oieq2  9492  ordtypelem1  9497  inf3lemc  9612  wemapwe  9683  ttrcleq  9695  r1sucg  9758  r1limg  9760  rankprb  9842  scotteqd  9894  karden  9923  kardenOLD  9924  djueq12  9934  cardiun  10012  acneq  10071  alephlim  10095  alephsuc  10096  alephfplem2  10133  infpssrlem2  10331  fin23lem34  10373  fin23lem35  10374  zorn2lem1  10523  zorn2lem7  10529  fpwwe2lem5  10669  fpwwe2lem12  10676  addpiord  10918  mulpiord  10919  addpqnq  10972  mulpqnq  10975  addassnq  10992  mulassnq  10993  distrnq  10995  lterpq  11004  ltexnq  11009  ltsrpr  11111  00sr  11133  recexsrlem  11137  mulgt0sr  11139  addcnsrec  11177  mulcnsrec  11178  negeq  11498  csbnegg  11503  negsubdi  11563  mulneg1  11699  negfi  12213  deceq1  12766  deceq2  12767  xnegeq  13284  fseq1p1m1  13678  om2uzrdg  14045  uzrdgsuci  14049  seqeq1  14093  seqeq2  14094  seqeq3  14095  seqfeq4  14140  seqof  14148  hashprg  14484  hashtpg  14575  csbwrdg  14634  s1eq  14692  cats1co  14952  s2eqd  14959  s3eqd  14960  s4eqd  14961  s5eqd  14962  s6eqd  14963  s7eqd  14964  s8eqd  14965  xpcogend  15072  shftval  15172  limsupgle  15589  lo1eq  15680  rlimeq  15681  sumeq1  15801  sumeq2w  15804  sumeq2ii  15805  sumeq2sdv  15815  zsum  15829  sumss2  15837  fsumsplitsnun  15866  isumclim3  15870  fsumcom2  15885  incexclem  15950  incexc2  15952  isumshft  15953  prodeq1f  16020  prodeq1  16021  prodeq2w  16024  prodeq2ii  16025  prodeq2sdv  16036  zprod  16049  fprodm1s  16082  fprodp1s  16083  fprodcom2  16096  fprodsplitf  16100  iprodclim3  16112  ef0lem  16189  ruclem7  16349  sadcp1  16570  smupp1  16595  smueqlem  16605  algrp1  16689  dfphi2  16890  prmdiveq  16902  pceulem  16962  vdwlem6  17103  cshwsiun  17216  sloteq  17300  setsid  17324  elbasfv  17332  elbasov  17333  imastset  17633  imasvscaval  17649  isoval  17879  funcoppc  17989  fulloppc  18038  fuccofval  18076  natpropd  18093  catccofval  18218  xpchomfval  18292  xpccofval  18295  lubfval  18461  glbfval  18474  chneq1  18725  chneq2  18726  grpidpropd  18781  gsumpropd2lem  18807  frmdplusg  18989  efmndplusg  19015  grpinvpropd  19164  grpsubpropd  19194  grpsubpropd2  19195  mulgpropd  19265  ecqusaddd  19346  oppgmnd  19507  sylow1lem2  19752  sylow3lem1  19780  prds1  20491  pwsmgp  20495  opprrng  20514  rngidpropd  20584  dvdsrpropd  20585  unitpropd  20586  invrpropd  20587  rhm1  20663  rhmopp  20698  rhmsubclem2  20877  lmhmpropd  21287  lidlrsppropd  21471  rngqiprnglinlem2  21527  lpival  21587  pzriprnglem11  21736  zrhpropd  21759  znle  21781  frlmplusgval  22009  frlmvscafval  22011  ressascl  22143  asclpropd  22144  aspval2  22145  psrbas  22181  psrplusg  22184  psrmulr  22189  psrvscafval  22195  resspsrbas  22220  ressmplbas2  22274  opsrle  22295  opsrbaslem  22297  vr1val  22449  ressply1add  22486  ressply1mul  22487  ressply1vsca  22488  psrplusgpropd  22492  mplbaspropd  22493  psropprmul  22494  ply1baspropd  22499  ply1plusgpropd  22500  ply1sca2  22510  ply1ascl0  22511  ply1ascl1  22512  subrgvr1  22519  coe1mul2lem2  22526  ply1coe1eq  22557  evls1addd  22628  evls1muld  22629  evls1vsca  22630  rhmply1vr1  22641  rhmply1vsca  22642  mamudi  22657  mamudir  22658  matrcl  22666  oftpos  22706  mattpos1  22710  mdetfval  22840  mdetrlin  22856  mdetrsca  22857  mdetrsca2  22858  mdetrlin2  22861  mdetunilem5  22870  madufval  22891  madugsum  22897  idmatidpmat  22994  cpmidpmat  23130  cncmp  23649  2ndcsep  23717  llyeq  23728  nllyeq  23729  xkouni  23857  hmphindis  24055  xkocnv  24072  ptcmplem2  24311  snclseqg  24374  prdstmdd  24382  ustexsym  24474  ucnextcn  24561  metreslem  24620  comet  24771  nrmmetd  24832  nmpropd  24852  isngp3  24856  ngpds  24862  subgnm  24891  tngnm  24909  idnghm  25001  cnmetdval  25028  cnmpopc  25188  htpyco2  25239  phtpyco2  25250  clsocv  25510  rrxprds  25649  rrxnm  25651  rrxplusgvscavalb  25655  ovolunlem1a  25756  voliunlem3  25812  ioombl1lem4  25821  uniioombllem4  25846  itg11  25951  itgeq1f  26031  itgeq1  26032  itgeq2  26037  iblss2  26065  itgss  26071  itgeqa  26073  itgfsum  26086  itgsplit  26095  ditgeq1  26107  ditgeq2  26108  ditgeq3  26109  dvcmulf  26204  dvmptfsum  26234  dvcnvrelem2  26277  mdegfval  26319  mdegpropd  26341  deg1propd  26343  plyeq0  26469  coe11  26511  dgrlt  26524  dgradd2  26526  dgrmulc  26529  dvply1  26546  fta1lem  26569  pserulm  26690  rlimcnp2  27235  jensenlem1  27255  basellem5  27353  dchrbas  27503  dchrrcl  27508  dchrplusg  27515  dchrfi  27523  lgsdi  27602  lgseisenlem2  27644  lgsquadlem3  27650  dchrmusumlema  27761  rpvmasum2  27780  dchrisum0lema  27782  pntlemg  27866  nosupbnd2lem1  27983  lruneq  28204  addsval  28259  mulsval  28406  seqseq123d  28583  colperpexlem2  29118  symquadmid  29215  tgaaddcpbllem2  29261  axlowdimlem13  29443  uhgrvtxedgiedgb  29625  nb3grprlem1  29872  crctcshlem2  30318  wpthswwlks2on  30464  clwlknf1oclwwlkn  30586  frgrncvvdeq  30821  avril1  30975  0vfval  31119  imsval  31198  imsdval  31199  bcseqi  31633  normpythi  31655  cm0  32122  fh1  32131  pjcji  32197  opsqrlem5  32657  pjsdi2i  32670  pjclem3  32710  pjci  32713  golem1  32784  iuneq12daf  33062  iunrdx  33069  ofresid  33147  cnvprop  33200  coprprop  33203  f1od2  33222  dp2eq1  33350  dp2eq2  33351  fzto1st1  33574  gsumvsca1  33698  gsumvsca2  33699  urpropd  33702  resv1r  33811  nsgqusf1olem2  33876  oppr2idl  33921  opprqus0g  33925  ressply1evls1  34008  esplyfvn  34120  vietalem  34122  lindsunlem  34167  fedgmullem1  34172  fedgmullem2  34173  fedgmul  34174  fldsdrgfldext2  34205  fldextrspunlem1  34218  fldextrspunfld  34219  algextdeglem4  34263  crefeq  34388  rspectopn  34410  xrge0mulc1cn  34484  qqhval2  34525  esumeq12dvaf  34574  esumeq2  34579  esumf1o  34593  esumfzf  34612  esumss  34615  esumpfinvalf  34619  ofceq  34640  carsgclctunlem1  34861  itgeq12dv  34870  ccatmulgnn0dir  35086  breprexpnat  35175  bnj956  35319  bnj1385  35374  bnj96  35407  bnj548  35439  bnj553  35440  bnj554  35441  bnj602  35457  bnj18eq1  35469  bnj1234  35555  bnj1296  35563  bnj1318  35567  bnj1442  35591  bnj1450  35592  cvmliftlem5  35951  cvmliftlem10  35956  cvmlift2lem9  35973  cvmliftphtlem  35979  satfdm  36031  mthmpps  36244  rdgprc  36454  dfrdg2  36455  wsuceq123  36474  wlimeq12  36479  altopthsn  36624  altxpeq1  36636  altxpeq2  36637  nmulprop  36837  ixpeq12dv  36903  prodeq12sdv  36905  itgeq12sdv  36906  ditgeq123dv  36908  cbvcsbdavw  36946  cbvcsbdavw2  36947  cbvrabdavw  36948  cbviundavw  36949  cbviindavw  36950  cbvopab1davw  36951  cbvopab2davw  36952  cbvopabdavw  36953  cbvmptdavw  36954  cbviotadavw  36956  cbvriotadavw  36957  cbvoprab1davw  36958  cbvoprab2davw  36959  cbvoprab3davw  36960  cbvoprab123davw  36961  cbvoprab12davw  36962  cbvoprab23davw  36963  cbvoprab13davw  36964  cbvixpdavw  36965  cbvsumdavw  36966  cbvproddavw  36967  cbvitgdavw  36968  cbvditgdavw  36969  cbvrabdavw2  36972  cbviundavw2  36973  cbviindavw2  36974  cbvmptdavw2  36975  cbvriotadavw2  36977  cbvmpodavw2  36978  cbvmpo1davw2  36979  cbvmpo2davw2  36980  cbvixpdavw2  36981  cbvsumdavw2  36982  cbvproddavw2  36983  cbvitgdavw2  36984  cbvditgdavw2  36985  ee7.2aOLD  37147  ttceq  37174  bj-sngleq  37778  bj-tageq  37787  bj-projeq  37803  bj-projval  37807  bj-1upleq  37810  bj-pr1eq  37813  bj-pr2eq  37827  bj-evaleq  37888  bj-imafv  38068  csbrecsg  38147  csbrdgg  38148  csboprabg  38149  csbmpo123  38150  finxpeq1  38205  finxpeq2  38206  csbfinxpg  38207  finxpreclem4  38213  unceq  38420  unccur  38422  finixpnum  38424  ptrest  38433  poimirlem3  38437  poimirlem9  38443  poimirlem15  38449  poimirlem16  38450  poimirlem26  38460  poimirlem27  38461  mbfposadd  38481  cnambfre  38482  iblabsnclem  38497  ftc1anclem1  38507  heiborlem4  38629  heiborlem6  38631  mpobi123f  38975  iineq12f  38977  mptbi12f  38979  eccnvepres  39099  xrneq1  39209  xrneq2  39212  shiftstableeq2  39296  cosseq  39329  redundss3  39525  riotaclbgBAD  39892  toycom  39911  ldualvbase  40064  ldualfvadd  40066  ldualsca  40070  ldualsbase  40071  ldualsaddN  40072  ldualfvs  40074  ldual0  40085  ldual1  40086  ldualneg  40087  cdleme19f  41246  cdleme20m  41261  cdleme21k  41276  cdleme27b  41306  cdleme31so  41317  cdleme31sn  41318  cdleme31se  41320  cdleme31se2  41321  cdleme31sc  41322  cdleme31sde  41323  cdleme31fv  41328  cdleme40v  41407  cdleme43dN  41430  cdlemeg46ngfr  41456  ltrnco4  41677  tgrpbase  41684  tgrpopr  41685  erngbase  41739  erngfplus  41740  erngfmul  41743  erngbase-rN  41747  erngfplus-rN  41748  erngfmul-rN  41751  dvasca  41944  dvavbase  41951  dvafvadd  41952  dvafvsca  41954  tendocnv  41959  dvhsca  42020  dvhfplusr  42022  dvhvbase  42025  dvhfvadd  42029  dvhfvsca  42038  lcdvadd  42535  lcdsbase  42538  lcdsadd  42539  lcdvs  42541  lcd0  42546  lcd1  42547  lcdneg  42548  fsuppind  43501  imaiinfv  43603  mapfzcons1  43627  rexrabdioph  43700  dnnumch1  43950  dnwech  43954  aomclem6  43965  pwssplit4  43995  pwfi2f1o  44002  mendplusgfval  44087  mendvscafval  44092  harval3  44443  dssmapntrcls  45033  colleq12d  45142  uzmptshftfval  45235  dropab1  45335  dropab2  45336  iineq12dv  46003  rabbida2  46029  rabbida3  46032  itgsinexplem1  46847  wallispi2lem2  46965  fourierdlem36  47036  etransclem4  47131  fcoreslem1  48016  afveq12d  48086  aoveq123d  48131  aovfundmoveq  48134  aovnuoveq  48144  aovvoveq  48145  aovovn0oveq  48147  afv2eq12d  48168  fsumsplitsndif  48334  rngccofvalALTV  49250  rhmsubcALTVlem2  49262  ringccofvalALTV  49284  itscnhlinecirc02plem2  49778  oppfrcl3  50121  oppf1st2nd  50122  uppropd  50172  natoppf  50220  catcrcl  50386  lmdpropd  50648  cmdpropd  50649  lmddu  50658  cmddu  50659  setrecseq  50676  aacllem  50837