Theorem 3eqtr4g 2795

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

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  rabbidva2  3432  rabbida4  3455  rabeqf  3464  rabeqiOLD  3469  csbeq1  3895  csbeq2  3897  csbeq2d  3898  difeq1  4114  difeq2  4115  uneq2  4156  ineq1  4204  ineq2  4205  symdifeq1  4243  symdifeq2  4244  dfrab3ss  4311  csbprc  4405  csbnestgfw  4418  csbnestgf  4423  disjssun  4466  ifeq1  4531  ifeq2  4532  pweqALT  4616  sneq  4637  csbsng  4711  csbprg  4712  preq1  4736  preq2  4737  tpeq1  4745  tpeq2  4746  tpeq3  4747  prprc1  4768  tpprceq3  4806  opeq1  4872  opeq2  4873  oteq1  4881  oteq2  4882  oteq3  4883  csbopg  4890  unieqOLD  4919  uniprg  4924  csbuni  4939  inteq  4952  iineq1  5013  iineq2  5016  iuneq12df  5022  dfiin2g  5034  iinrab  5071  iinin1  5081  iinxprg  5091  iununi  5101  opabbid  5212  opabbidv  5213  mpteq12da  5232  mpteq12dfOLD  5234  mpteq12f  5235  mpteq12dva  5236  csbmpt12  5556  xpeq1  5689  xpeq2  5696  rneq  5934  reseq1  5974  reseq2  5975  resima2  6015  resindm  6029  resmpt  6036  resmptf  6038  imaeq1  6053  imaeq2  6054  mptcnv  6138  xpdisj1  6159  xpdisj2  6160  resdisj  6167  dmpropg  6213  rnpropg  6220  cores  6247  cores2  6257  xpco  6287  predeq123  6300  csbpredg  6305  sspred  6308  predres  6339  suceq  6429  sucprc  6439  iotaeq  6507  iotabi  6508  fntpg  6607  imain  6632  f1oprswap  6876  fveq1  6889  fveq2  6890  fvres  6909  csbfv12  6938  fnimapr  6974  fvco2  6987  xpprsng  7139  residpr  7142  fsnunfv  7186  fsnunres  7187  funiunfv  7249  f1ofvswap  7306  fliftf  7314  isoini2  7338  eqfunressuc  7360  riotaeqdv  7368  riotabidv  7369  riotauni  7373  riotabidva  7387  snriota  7401  oveq  7417  oveq1  7418  oveq2  7419  oprabbid  7476  oprabbidv  7477  mpoeq123  7483  mpoeq123dva  7485  mpoeq3dva  7488  resmpo  7530  ovres  7575  f1ocnvd  7659  ofeqd  7674  ofreq  7676  fpar  8104  frecseq123  8269  csbfrecsg  8271  wrecseq123  8301  wrecseq123OLD  8302  csbwrecsg  8308  onovuni  8344  recseq  8376  tfr2a  8397  rdgeq1  8413  rdgeq2  8414  rdgsucmptf  8430  frsucmpt  8440  seqomeq12  8456  seqomsuc  8459  omopthi  8662  eceq1  8743  eceq2  8745  qseq1  8759  qseq2  8760  uniqs  8773  ecinxp  8788  qsinxp  8789  erovlem  8809  ecopovtrn  8816  ixpeq1  8904  unfi  9174  supeq1  9442  supeq2  9445  supeq3  9446  supeq123d  9447  infeq1  9473  infeq2  9476  infeq3  9477  infeq123d  9478  infiso  9505  oieq1  9509  oieq2  9510  ordtypelem1  9515  inf3lemc  9623  wemapwe  9694  ttrcleq  9706  r1sucg  9766  r1limg  9768  rankprb  9848  karden  9892  djueq12  9901  cardiun  9979  acneq  10040  alephlim  10064  alephsuc  10065  alephfplem2  10102  infpssrlem2  10301  fin23lem34  10343  fin23lem35  10344  zorn2lem1  10493  zorn2lem7  10499  fpwwe2lem5  10632  fpwwe2lem12  10639  addpiord  10881  mulpiord  10882  addpqnq  10935  mulpqnq  10938  addassnq  10955  mulassnq  10956  distrnq  10958  lterpq  10967  ltexnq  10972  ltsrpr  11074  00sr  11096  recexsrlem  11100  mulgt0sr  11102  addcnsrec  11140  mulcnsrec  11141  negeq  11456  csbnegg  11461  negsubdi  11520  mulneg1  11654  negfi  12167  deceq1  12686  deceq2  12687  xnegeq  13190  fseq1p1m1  13579  om2uzrdg  13925  uzrdgsuci  13929  seqeq1  13973  seqeq2  13974  seqeq3  13975  seqfeq4  14021  seqof  14029  hashprg  14359  hashtpg  14450  csbwrdg  14498  s1eq  14554  cats1co  14811  s2eqd  14818  s3eqd  14819  s4eqd  14820  s5eqd  14821  s6eqd  14822  s7eqd  14823  s8eqd  14824  xpcogend  14925  shftval  15025  limsupgle  15425  lo1eq  15516  rlimeq  15517  sumeq1  15639  sumeq2w  15642  sumeq2ii  15643  zsum  15668  sumss2  15676  fsumsplitsnun  15705  isumclim3  15709  fsumcom2  15724  incexclem  15786  incexc2  15788  isumshft  15789  prodeq1f  15856  prodeq2w  15860  prodeq2ii  15861  zprod  15885  fprodm1s  15918  fprodp1s  15919  fprodcom2  15932  fprodsplitf  15936  iprodclim3  15948  ef0lem  16026  ruclem7  16183  sadcp1  16400  smupp1  16425  smueqlem  16435  algrp1  16515  dfphi2  16711  prmdiveq  16723  pceulem  16782  vdwlem6  16923  cshwsiun  17037  sloteq  17120  setsid  17145  elbasfv  17154  elbasov  17155  imastset  17472  imasvscaval  17488  isoval  17716  funcoppc  17829  fulloppc  17877  fuccofval  17915  natpropd  17933  catccofval  18058  xpchomfval  18135  xpccofval  18138  lubfval  18307  glbfval  18320  grpidpropd  18587  gsumpropd2lem  18604  frmdplusg  18771  efmndplusg  18797  grpinvpropd  18934  grpsubpropd  18964  grpsubpropd2  18965  mulgpropd  19032  ecqusaddd  19107  oppgmnd  19262  sylow1lem2  19508  sylow3lem1  19536  prds1  20211  pwsmgp  20215  opprrng  20236  rngidpropd  20306  dvdsrpropd  20307  unitpropd  20308  invrpropd  20309  rhm1  20380  rhmopp  20400  lmhmpropd  20828  lidlrsppropd  21004  rngqiprnglinlem2  21051  lpival  21083  pzriprnglem11  21260  zrhpropd  21283  znle  21307  frlmplusgval  21538  frlmvscafval  21540  ressascl  21669  asclpropd  21670  aspval2  21671  psrbas  21716  psrplusg  21719  psrmulr  21722  psrvscafval  21728  resspsrbas  21754  ressmplbas2  21801  opsrle  21821  opsrbaslem  21823  opsrbaslemOLD  21824  vr1val  21935  ressply1add  21972  ressply1mul  21973  ressply1vsca  21974  psrplusgpropd  21978  mplbaspropd  21979  psropprmul  21980  ply1baspropd  21985  ply1plusgpropd  21986  ply1sca2  21996  subrgvr1  22003  coe1mul2lem2  22010  ply1coe1eq  22042  mamudi  22123  mamudir  22124  matrcl  22132  oftpos  22174  mattpos1  22178  mdetfval  22308  mdetrlin  22324  mdetrsca  22325  mdetrsca2  22326  mdetrlin2  22329  mdetunilem5  22338  madufval  22359  madugsum  22365  idmatidpmat  22459  cpmidpmat  22595  cncmp  23116  2ndcsep  23183  llyeq  23194  nllyeq  23195  xkouni  23323  hmphindis  23521  xkocnv  23538  ptcmplem2  23777  snclseqg  23840  prdstmdd  23848  ustexsym  23940  ucnextcn  24029  metreslem  24088  comet  24242  nrmmetd  24303  nmpropd  24323  isngp3  24327  ngpds  24333  subgnm  24362  tngnm  24388  idnghm  24480  cnmetdval  24507  cnmpopc  24669  htpyco2  24725  phtpyco2  24736  clsocv  24998  rrxprds  25137  rrxnm  25139  rrxplusgvscavalb  25143  ovolunlem1a  25245  voliunlem3  25301  ioombl1lem4  25310  uniioombllem4  25335  itg11  25440  itgeq1f  25521  itgeq2  25527  iblss2  25555  itgss  25561  itgeqa  25563  itgfsum  25576  itgsplit  25585  ditgeq1  25597  ditgeq2  25598  ditgeq3  25599  dvcmulf  25696  dvmptfsum  25727  dvcnvrelem2  25770  mdegfval  25815  mdegpropd  25837  deg1propd  25839  plyeq0  25960  coe11  26002  dgrlt  26016  dgradd2  26018  dgrmulc  26021  dvply1  26033  fta1lem  26056  pserulm  26170  rlimcnp2  26707  jensenlem1  26727  basellem5  26825  dchrbas  26974  dchrrcl  26979  dchrplusg  26986  dchrfi  26994  lgsdi  27073  lgseisenlem2  27115  lgsquadlem3  27121  dchrmusumlema  27232  rpvmasum2  27251  dchrisum0lema  27253  pntlemg  27337  nosupbnd2lem1  27454  lruneq  27637  addsval  27684  mulsval  27804  colperpexlem2  28249  axlowdimlem13  28479  uhgrvtxedgiedgb  28663  nb3grprlem1  28904  crctcshlem2  29339  wpthswwlks2on  29482  clwlknf1oclwwlkn  29604  frgrncvvdeq  29829  avril1  29983  0vfval  30126  imsval  30205  imsdval  30206  bcseqi  30640  normpythi  30662  cm0  31129  fh1  31138  pjcji  31204  opsqrlem5  31664  pjsdi2i  31677  pjclem3  31717  pjci  31720  golem1  31791  iuneq12daf  32055  iunrdx  32062  ofresid  32134  fnimatp  32169  cnvprop  32185  coprprop  32188  f1od2  32213  dp2eq1  32306  dp2eq2  32307  fzto1st1  32531  gsumvsca1  32641  gsumvsca2  32642  urpropd  32648  resv1r  32726  nsgqusf1olem2  32799  oppr2idl  32874  opprqus0g  32878  evls1addd  32922  evls1muld  32923  evls1vsca  32924  ply1ascl0  32926  ply1ascl1  32927  lindsunlem  32997  fedgmullem1  33002  fedgmullem2  33003  fedgmul  33004  algextdeglem4  33065  crefeq  33123  rspectopn  33145  xrge0mulc1cn  33219  qqhval2  33260  esumeq12dvaf  33327  esumeq2  33332  esumf1o  33346  esumfzf  33365  esumss  33368  esumpfinvalf  33372  ofceq  33393  carsgclctunlem1  33614  itgeq12dv  33623  ccatmulgnn0dir  33851  breprexpnat  33944  bnj956  34085  bnj1385  34141  bnj96  34174  bnj548  34206  bnj553  34207  bnj554  34208  bnj602  34224  bnj18eq1  34236  bnj1234  34322  bnj1296  34330  bnj1318  34334  bnj1442  34358  bnj1450  34359  cvmliftlem5  34578  cvmliftlem10  34583  cvmlift2lem9  34600  cvmliftphtlem  34606  satfdm  34658  mthmpps  34871  rdgprc  35070  dfrdg2  35071  wsuceq123  35090  wlimeq12  35095  altopthsn  35237  altxpeq1  35249  altxpeq2  35250  ee7.2aOLD  35649  bj-sngleq  36151  bj-tageq  36160  bj-projeq  36176  bj-projval  36180  bj-1upleq  36183  bj-pr1eq  36186  bj-pr2eq  36200  bj-evaleq  36256  bj-imafv  36435  csbrecsg  36512  csbrdgg  36513  csboprabg  36514  csbmpo123  36515  finxpeq1  36570  finxpeq2  36571  csbfinxpg  36572  finxpreclem4  36578  cureq  36767  unceq  36768  uncov  36772  unccur  36774  finixpnum  36776  ptrest  36790  poimirlem3  36794  poimirlem9  36800  poimirlem15  36806  poimirlem16  36807  poimirlem26  36817  poimirlem27  36818  mbfposadd  36838  cnambfre  36839  iblabsnclem  36854  ftc1anclem1  36864  heiborlem4  36985  heiborlem6  36987  mpobi123f  37333  iineq12f  37335  mptbi12f  37337  eccnvepres  37451  uniqsALTV  37501  xrneq1  37550  xrneq2  37553  cosseq  37599  redundss3  37801  riotaclbgBAD  38127  toycom  38146  ldualvbase  38299  ldualfvadd  38301  ldualsca  38305  ldualsbase  38306  ldualsaddN  38307  ldualfvs  38309  ldual0  38320  ldual1  38321  ldualneg  38322  cdleme19f  39482  cdleme20m  39497  cdleme21k  39512  cdleme27b  39542  cdleme31so  39553  cdleme31sn  39554  cdleme31se  39556  cdleme31se2  39557  cdleme31sc  39558  cdleme31sde  39559  cdleme31fv  39564  cdleme40v  39643  cdleme43dN  39666  cdlemeg46ngfr  39692  ltrnco4  39913  tgrpbase  39920  tgrpopr  39921  erngbase  39975  erngfplus  39976  erngfmul  39979  erngbase-rN  39983  erngfplus-rN  39984  erngfmul-rN  39987  dvasca  40180  dvavbase  40187  dvafvadd  40188  dvafvsca  40190  tendocnv  40195  dvhsca  40256  dvhfplusr  40258  dvhvbase  40261  dvhfvadd  40265  dvhfvsca  40274  lcdvadd  40771  lcdsbase  40774  lcdsadd  40775  lcdvs  40777  lcd0  40782  lcd1  40783  lcdneg  40784  fsuppind  41464  imaiinfv  41733  mapfzcons1  41757  rexrabdioph  41834  dnnumch1  42088  dnwech  42092  aomclem6  42103  pwssplit4  42133  pwfi2f1o  42140  mendplusgfval  42229  mendvscafval  42234  harval3  42591  dssmapntrcls  43181  scotteqd  43298  colleq12d  43314  uzmptshftfval  43407  dropab1  43508  dropab2  43509  rabbida2  44122  rabbida3  44125  itgsinexplem1  44968  wallispi2lem2  45086  fourierdlem36  45157  etransclem4  45252  fcoreslem1  46071  afveq12d  46139  aoveq123d  46184  aovfundmoveq  46187  aovnuoveq  46197  aovvoveq  46198  aovovn0oveq  46200  afv2eq12d  46221  fsumsplitsndif  46339  rngccofvalALTV  46973  ringccofvalALTV  47036  rhmsubclem2  47073  rhmsubcALTVlem2  47091  itscnhlinecirc02plem2  47556  setrecseq  47817  aacllem  47935