Theorem 3eqtr4g 2829

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

Syntax hints:   → wi 4   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  rabbidva2  3424  rabbida4  3447  csbeq1  3862  csbeq2  3864  csbeq2d  3865  csbeq2dv  3866  difeq1  4080  difeq2  4081  uneq2  4122  ineq1  4172  ineq2  4173  symdifeq1  4214  symdifeq2  4215  dfrab3ss  4282  csbprc  4378  csbnestgfw  4391  csbnestgf  4396  disjssun  4432  ifeq1  4494  ifeq2  4495  pweqALT  4580  sneq  4602  csbsng  4677  csbprg  4678  preq1  4702  preq2  4703  tpeq1  4711  tpeq2  4712  tpeq3  4713  prprc1  4734  tpprceq3  4774  opeq1  4840  opeq2  4841  oteq1  4849  oteq2  4850  oteq3  4851  csbopg  4858  uniprg  4890  csbuni  4905  inteq  4917  iineq1  4976  iineq2  4979  iuneq12df  4985  iuneq12d  4988  dfiin2g  4997  iinrab  5035  iinin1  5047  iinxprg  5057  iununi  5067  opabbid  5178  opabbidv  5179  mpteq12da  5196  mpteq12f  5198  mpteq12dva  5199  csbmpt12  5543  xpeq1  5676  xpeq2  5683  rneq  5927  reseq1  5973  reseq2  5974  resima2  6016  resindmOLD  6031  resmpt  6040  resmptf  6042  imaeq1  6058  imaeq2  6059  mptcnv  6139  xpdisj1  6159  xpdisj2  6160  resdisj  6168  dmpropg  6217  rnpropg  6224  cores  6251  cores2  6262  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  7137  residpr  7140  fsnunfv  7186  fsnunres  7187  funiunfv  7247  f1ofvswap  7305  fliftf  7314  isoini2  7338  eqfunressuc  7360  riotaeqdv  7369  riotabidv  7370  riotauni  7374  riotabidva  7387  snriota  7401  oveq  7417  oveq1  7418  oveq2  7419  oprabbid  7476  oprabbidv  7477  mpoeq123  7483  mpoeq123dva  7485  mpoeq3dva  7488  resmpo  7531  ovres  7577  f1ocnvd  7662  ofeqd  7677  ofreq  7679  fpar  8111  frecseq123  8279  csbfrecsg  8281  wrecseq123  8310  csbwrecsg  8315  onovuni  8329  recseq  8360  tfr2a  8382  rdgeq1  8398  rdgeq2  8399  rdgsucmptf  8415  frsucmpt  8425  seqomeq12  8441  seqomsuc  8444  omopthi  8647  eceq1  8734  eceq2  8736  qseq1  8754  qseq2  8755  uniqs  8771  snecg  8775  ecinxp  8790  qsinxp  8791  erovlem  8811  ecopovtrn  8818  ixpeq1  8906  unfi  9155  supeq1  9405  supeq2  9408  supeq3  9409  supeq123d  9410  infeq1  9437  infeq2  9440  infeq3  9441  infeq123d  9442  infiso  9470  oieq1  9474  oieq2  9475  ordtypelem1  9480  inf3lemc  9595  wemapwe  9666  ttrcleq  9678  r1sucg  9741  r1limg  9743  rankprb  9823  scotteqd  9863  karden  9881  djueq12  9890  cardiun  9968  acneq  10027  alephlim  10051  alephsuc  10052  alephfplem2  10089  infpssrlem2  10288  fin23lem34  10330  fin23lem35  10331  zorn2lem1  10480  zorn2lem7  10486  fpwwe2lem5  10620  fpwwe2lem12  10627  addpiord  10869  mulpiord  10870  addpqnq  10923  mulpqnq  10926  addassnq  10943  mulassnq  10944  distrnq  10946  lterpq  10955  ltexnq  10960  ltsrpr  11062  00sr  11084  recexsrlem  11088  mulgt0sr  11090  addcnsrec  11128  mulcnsrec  11129  negeq  11449  csbnegg  11454  negsubdi  11514  mulneg1  11650  negfi  12164  deceq1  12716  deceq2  12717  xnegeq  13233  fseq1p1m1  13626  om2uzrdg  13992  uzrdgsuci  13996  seqeq1  14040  seqeq2  14041  seqeq3  14042  seqfeq4  14087  seqof  14095  hashprg  14431  hashtpg  14522  csbwrdg  14581  s1eq  14638  cats1co  14893  s2eqd  14900  s3eqd  14901  s4eqd  14902  s5eqd  14903  s6eqd  14904  s7eqd  14905  s8eqd  14906  xpcogend  15011  shftval  15111  limsupgle  15528  lo1eq  15619  rlimeq  15620  sumeq1  15740  sumeq2w  15743  sumeq2ii  15744  sumeq2sdv  15754  zsum  15769  sumss2  15777  fsumsplitsnun  15806  isumclim3  15810  fsumcom2  15825  incexclem  15890  incexc2  15892  isumshft  15893  prodeq1f  15960  prodeq1  15961  prodeq2w  15964  prodeq2ii  15965  prodeq2sdv  15977  zprod  15991  fprodm1s  16024  fprodp1s  16025  fprodcom2  16038  fprodsplitf  16042  iprodclim3  16054  ef0lem  16132  ruclem7  16292  sadcp1  16513  smupp1  16538  smueqlem  16548  algrp1  16632  dfphi2  16833  prmdiveq  16845  pceulem  16905  vdwlem6  17046  cshwsiun  17159  sloteq  17243  setsid  17267  elbasfv  17275  elbasov  17276  imastset  17576  imasvscaval  17592  isoval  17822  funcoppc  17932  fulloppc  17981  fuccofval  18019  natpropd  18036  catccofval  18161  xpchomfval  18235  xpccofval  18238  lubfval  18404  glbfval  18417  chneq1  18668  chneq2  18669  grpidpropd  18720  gsumpropd2lem  18737  frmdplusg  18913  efmndplusg  18939  grpinvpropd  19081  grpsubpropd  19111  grpsubpropd2  19112  mulgpropd  19182  ecqusaddd  19263  oppgmnd  19424  sylow1lem2  19669  sylow3lem1  19697  prds1  20404  pwsmgp  20408  opprrng  20427  rngidpropd  20497  dvdsrpropd  20498  unitpropd  20499  invrpropd  20500  rhm1  20571  rhmopp  20592  rhmsubclem2  20771  lmhmpropd  21172  lidlrsppropd  21352  rngqiprnglinlem2  21403  lpival  21461  pzriprnglem11  21610  zrhpropd  21633  znle  21655  frlmplusgval  21883  frlmvscafval  21885  ressascl  22015  asclpropd  22016  aspval2  22017  psrbas  22053  psrplusg  22056  psrmulr  22061  psrvscafval  22067  resspsrbas  22092  ressmplbas2  22146  opsrle  22167  opsrbaslem  22169  vr1val  22321  ressply1add  22358  ressply1mul  22359  ressply1vsca  22360  psrplusgpropd  22364  mplbaspropd  22365  psropprmul  22366  ply1baspropd  22371  ply1plusgpropd  22372  ply1sca2  22382  ply1ascl0  22383  ply1ascl1  22384  subrgvr1  22391  coe1mul2lem2  22398  ply1coe1eq  22429  evls1addd  22500  evls1muld  22501  evls1vsca  22502  rhmply1vr1  22513  rhmply1vsca  22514  mamudi  22529  mamudir  22530  matrcl  22538  oftpos  22578  mattpos1  22582  mdetfval  22712  mdetrlin  22728  mdetrsca  22729  mdetrsca2  22730  mdetrlin2  22733  mdetunilem5  22742  madufval  22763  madugsum  22769  idmatidpmat  22863  cpmidpmat  22999  cncmp  23518  2ndcsep  23585  llyeq  23596  nllyeq  23597  xkouni  23725  hmphindis  23923  xkocnv  23940  ptcmplem2  24179  snclseqg  24242  prdstmdd  24250  ustexsym  24342  ucnextcn  24429  metreslem  24488  comet  24639  nrmmetd  24700  nmpropd  24720  isngp3  24724  ngpds  24730  subgnm  24759  tngnm  24777  idnghm  24869  cnmetdval  24896  cnmpopc  25056  htpyco2  25107  phtpyco2  25118  clsocv  25378  rrxprds  25517  rrxnm  25519  rrxplusgvscavalb  25523  ovolunlem1a  25624  voliunlem3  25680  ioombl1lem4  25689  uniioombllem4  25714  itg11  25819  itgeq1f  25899  itgeq1fOLD  25900  itgeq1  25901  itgeq2  25906  iblss2  25934  itgss  25940  itgeqa  25942  itgfsum  25955  itgsplit  25964  ditgeq1  25976  ditgeq2  25977  ditgeq3  25978  dvcmulf  26073  dvmptfsum  26103  dvcnvrelem2  26146  mdegfval  26188  mdegpropd  26210  deg1propd  26212  plyeq0  26337  coe11  26379  dgrlt  26392  dgradd2  26394  dgrmulc  26397  dvply1  26414  fta1lem  26437  pserulm  26551  rlimcnp2  27097  jensenlem1  27117  basellem5  27215  dchrbas  27365  dchrrcl  27370  dchrplusg  27377  dchrfi  27385  lgsdi  27464  lgseisenlem2  27506  lgsquadlem3  27512  dchrmusumlema  27623  rpvmasum2  27642  dchrisum0lema  27644  pntlemg  27728  nosupbnd2lem1  27845  lruneq  28066  addsval  28121  mulsval  28268  seqseq123d  28445  colperpexlem2  28971  axlowdimlem13  29245  uhgrvtxedgiedgb  29427  nb3grprlem1  29671  crctcshlem2  30108  wpthswwlks2on  30254  clwlknf1oclwwlkn  30376  frgrncvvdeq  30601  avril1  30755  0vfval  30899  imsval  30978  imsdval  30979  bcseqi  31413  normpythi  31435  cm0  31902  fh1  31911  pjcji  31977  opsqrlem5  32437  pjsdi2i  32450  pjclem3  32490  pjci  32493  golem1  32564  iuneq12daf  32842  iunrdx  32849  ofresid  32928  cnvprop  32982  coprprop  32985  f1od2  33005  dp2eq1  33133  dp2eq2  33134  fzto1st1  33363  gsumvsca1  33487  gsumvsca2  33488  urpropd  33491  resv1r  33602  nsgqusf1olem2  33667  oppr2idl  33713  opprqus0g  33717  ressply1evls1  33800  esplyfvn  33912  vietalem  33914  lindsunlem  33959  fedgmullem1  33964  fedgmullem2  33965  fedgmul  33966  fldsdrgfldext2  33997  fldextrspunlem1  34010  fldextrspunfld  34011  algextdeglem4  34055  crefeq  34180  rspectopn  34202  xrge0mulc1cn  34276  qqhval2  34317  esumeq12dvaf  34366  esumeq2  34371  esumf1o  34385  esumfzf  34404  esumss  34407  esumpfinvalf  34411  ofceq  34432  carsgclctunlem1  34652  itgeq12dv  34661  ccatmulgnn0dir  34877  breprexpnat  34966  bnj956  35110  bnj1385  35165  bnj96  35198  bnj548  35230  bnj553  35231  bnj554  35232  bnj602  35248  bnj18eq1  35260  bnj1234  35346  bnj1296  35354  bnj1318  35358  bnj1442  35382  bnj1450  35383  cvmliftlem5  35714  cvmliftlem10  35719  cvmlift2lem9  35736  cvmliftphtlem  35742  satfdm  35794  mthmpps  36007  rdgprc  36217  dfrdg2  36218  wsuceq123  36237  wlimeq12  36242  altopthsn  36386  altxpeq1  36398  altxpeq2  36399  nmulprop  36615  ixpeq12dv  36651  prodeq12sdv  36653  itgeq12sdv  36654  ditgeq123dv  36656  cbvcsbdavw  36694  cbvcsbdavw2  36695  cbvrabdavw  36696  cbviundavw  36697  cbviindavw  36698  cbvopab1davw  36699  cbvopab2davw  36700  cbvopabdavw  36701  cbvmptdavw  36702  cbviotadavw  36704  cbvriotadavw  36705  cbvoprab1davw  36706  cbvoprab2davw  36707  cbvoprab3davw  36708  cbvoprab123davw  36709  cbvoprab12davw  36710  cbvoprab23davw  36711  cbvoprab13davw  36712  cbvixpdavw  36713  cbvsumdavw  36714  cbvproddavw  36715  cbvitgdavw  36716  cbvditgdavw  36717  cbvrabdavw2  36720  cbviundavw2  36721  cbviindavw2  36722  cbvmptdavw2  36723  cbvriotadavw2  36725  cbvmpodavw2  36726  cbvmpo1davw2  36727  cbvmpo2davw2  36728  cbvixpdavw2  36729  cbvsumdavw2  36730  cbvproddavw2  36731  cbvitgdavw2  36732  cbvditgdavw2  36733  ee7.2aOLD  36895  ttceq  36922  bj-sngleq  37526  bj-tageq  37535  bj-projeq  37551  bj-projval  37555  bj-1upleq  37558  bj-pr1eq  37561  bj-pr2eq  37575  bj-evaleq  37636  bj-imafv  37818  csbrecsg  37897  csbrdgg  37898  csboprabg  37899  csbmpo123  37900  finxpeq1  37955  finxpeq2  37956  csbfinxpg  37957  finxpreclem4  37963  cureq  38170  unceq  38171  uncov  38175  unccur  38177  finixpnum  38179  ptrest  38193  poimirlem3  38197  poimirlem9  38203  poimirlem15  38209  poimirlem16  38210  poimirlem26  38220  poimirlem27  38221  mbfposadd  38241  cnambfre  38242  iblabsnclem  38257  ftc1anclem1  38267  heiborlem4  38388  heiborlem6  38390  mpobi123f  38736  iineq12f  38738  mptbi12f  38740  eccnvepres  38860  xrneq1  38970  xrneq2  38973  shiftstableeq2  39057  cosseq  39090  redundss3  39286  riotaclbgBAD  39653  toycom  39672  ldualvbase  39825  ldualfvadd  39827  ldualsca  39831  ldualsbase  39832  ldualsaddN  39833  ldualfvs  39835  ldual0  39846  ldual1  39847  ldualneg  39848  cdleme19f  41007  cdleme20m  41022  cdleme21k  41037  cdleme27b  41067  cdleme31so  41078  cdleme31sn  41079  cdleme31se  41081  cdleme31se2  41082  cdleme31sc  41083  cdleme31sde  41084  cdleme31fv  41089  cdleme40v  41168  cdleme43dN  41191  cdlemeg46ngfr  41217  ltrnco4  41438  tgrpbase  41445  tgrpopr  41446  erngbase  41500  erngfplus  41501  erngfmul  41504  erngbase-rN  41508  erngfplus-rN  41509  erngfmul-rN  41512  dvasca  41705  dvavbase  41712  dvafvadd  41713  dvafvsca  41715  tendocnv  41720  dvhsca  41781  dvhfplusr  41783  dvhvbase  41786  dvhfvadd  41790  dvhfvsca  41799  lcdvadd  42296  lcdsbase  42299  lcdsadd  42300  lcdvs  42302  lcd0  42307  lcd1  42308  lcdneg  42309  fsuppind  43249  imaiinfv  43351  mapfzcons1  43375  rexrabdioph  43448  dnnumch1  43698  dnwech  43702  aomclem6  43713  pwssplit4  43743  pwfi2f1o  43750  mendplusgfval  43835  mendvscafval  43840  harval3  44191  dssmapntrcls  44781  colleq12d  44890  uzmptshftfval  44983  dropab1  45083  dropab2  45084  iineq12dv  45751  rabbida2  45777  rabbida3  45780  itgsinexplem1  46595  wallispi2lem2  46713  fourierdlem36  46784  etransclem4  46879  fcoreslem1  47724  afveq12d  47794  aoveq123d  47839  aovfundmoveq  47842  aovnuoveq  47852  aovvoveq  47853  aovovn0oveq  47855  afv2eq12d  47876  fsumsplitsndif  48042  rngccofvalALTV  48959  rhmsubcALTVlem2  48971  ringccofvalALTV  48993  itscnhlinecirc02plem2  49483  oppfrcl3  49828  oppf1st2nd  49829  uppropd  49879  natoppf  49927  catcrcl  50093  lmdpropd  50355  cmdpropd  50356  lmddu  50365  cmddu  50366  setrecseq  50383  aacllem  50510