Theorem 3eqtr4g 2789

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

Syntax hints:   → wi 4   = wceq 1540

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 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  rabbidva2  3396  rabbida4  3420  rabeqf  3429  csbeq1  3854  csbeq2  3856  csbeq2d  3857  csbeq2dv  3858  difeq1  4070  difeq2  4071  uneq2  4113  ineq1  4164  ineq2  4165  symdifeq1  4206  symdifeq2  4207  dfrab3ss  4274  csbprc  4360  csbnestgfw  4373  csbnestgf  4378  disjssun  4419  ifeq1  4480  ifeq2  4481  pweqALT  4566  sneq  4587  rabsneq  4596  csbsng  4660  csbprg  4661  preq1  4685  preq2  4686  tpeq1  4694  tpeq2  4695  tpeq3  4696  prprc1  4717  tpprceq3  4755  opeq1  4824  opeq2  4825  oteq1  4833  oteq2  4834  oteq3  4835  csbopg  4842  uniprg  4874  csbuni  4887  inteq  4899  iineq1  4959  iineq2  4962  iuneq12df  4968  iuneq12d  4971  dfiin2g  4981  iinrab  5018  iinin1  5028  iinxprg  5038  iununi  5048  opabbid  5157  opabbidv  5158  mpteq12da  5175  mpteq12f  5177  mpteq12dva  5178  csbmpt12  5500  xpeq1  5633  xpeq2  5640  rneq  5878  reseq1  5924  reseq2  5925  resima2  5967  resindm  5981  resmpt  5988  resmptf  5990  imaeq1  6006  imaeq2  6007  mptcnv  6088  xpdisj1  6110  xpdisj2  6111  resdisj  6118  dmpropg  6164  rnpropg  6171  cores  6198  cores2  6208  xpco  6237  predeq123  6250  csbpredg  6255  sspred  6258  predres  6287  suceqd  6374  sucprc  6385  iotaeq  6450  iotabi  6451  fntpg  6542  imain  6567  f1oprswap  6808  fveq1  6821  fveq2  6822  fvres  6841  csbfv12  6868  fnimapr  6906  fnimatpd  6907  fvco2  6920  xpprsng  7074  residpr  7077  fsnunfv  7123  fsnunres  7124  funiunfv  7184  f1ofvswap  7243  fliftf  7252  isoini2  7276  eqfunressuc  7298  riotaeqdv  7307  riotabidv  7308  riotauni  7312  riotabidva  7325  snriota  7339  oveq  7355  oveq1  7356  oveq2  7357  oprabbid  7414  oprabbidv  7415  mpoeq123  7421  mpoeq123dva  7423  mpoeq3dva  7426  resmpo  7469  ovres  7515  f1ocnvd  7600  ofeqd  7615  ofreq  7617  fpar  8049  frecseq123  8215  csbfrecsg  8217  wrecseq123  8246  csbwrecsg  8251  onovuni  8265  recseq  8296  tfr2a  8317  rdgeq1  8333  rdgeq2  8334  rdgsucmptf  8350  frsucmpt  8360  seqomeq12  8376  seqomsuc  8379  omopthi  8579  eceq1  8664  eceq2  8666  qseq1  8684  qseq2  8685  uniqs  8701  ecinxp  8719  qsinxp  8720  erovlem  8740  ecopovtrn  8747  ixpeq1  8835  unfi  9085  supeq1  9335  supeq2  9338  supeq3  9339  supeq123d  9340  infeq1  9367  infeq2  9370  infeq3  9371  infeq123d  9372  infiso  9400  oieq1  9404  oieq2  9405  ordtypelem1  9410  inf3lemc  9522  wemapwe  9593  ttrcleq  9605  r1sucg  9665  r1limg  9667  rankprb  9747  karden  9791  djueq12  9800  cardiun  9878  acneq  9937  alephlim  9961  alephsuc  9962  alephfplem2  9999  infpssrlem2  10198  fin23lem34  10240  fin23lem35  10241  zorn2lem1  10390  zorn2lem7  10396  fpwwe2lem5  10529  fpwwe2lem12  10536  addpiord  10778  mulpiord  10779  addpqnq  10832  mulpqnq  10835  addassnq  10852  mulassnq  10853  distrnq  10855  lterpq  10864  ltexnq  10869  ltsrpr  10971  00sr  10993  recexsrlem  10997  mulgt0sr  10999  addcnsrec  11037  mulcnsrec  11038  negeq  11355  csbnegg  11360  negsubdi  11420  mulneg1  11556  negfi  12074  deceq1  12596  deceq2  12597  xnegeq  13109  fseq1p1m1  13501  om2uzrdg  13863  uzrdgsuci  13867  seqeq1  13911  seqeq2  13912  seqeq3  13913  seqfeq4  13958  seqof  13966  hashprg  14302  hashtpg  14392  csbwrdg  14451  s1eq  14507  cats1co  14763  s2eqd  14770  s3eqd  14771  s4eqd  14772  s5eqd  14773  s6eqd  14774  s7eqd  14775  s8eqd  14776  xpcogend  14881  shftval  14981  limsupgle  15384  lo1eq  15475  rlimeq  15476  sumeq1  15596  sumeq2w  15599  sumeq2ii  15600  sumeq2sdv  15610  zsum  15625  sumss2  15633  fsumsplitsnun  15662  isumclim3  15666  fsumcom2  15681  incexclem  15743  incexc2  15745  isumshft  15746  prodeq1f  15813  prodeq1  15814  prodeq2w  15817  prodeq2ii  15818  prodeq2sdv  15830  zprod  15844  fprodm1s  15877  fprodp1s  15878  fprodcom2  15891  fprodsplitf  15895  iprodclim3  15907  ef0lem  15985  ruclem7  16145  sadcp1  16366  smupp1  16391  smueqlem  16401  algrp1  16485  dfphi2  16685  prmdiveq  16697  pceulem  16757  vdwlem6  16898  cshwsiun  17011  sloteq  17094  setsid  17118  elbasfv  17126  elbasov  17127  imastset  17426  imasvscaval  17442  isoval  17672  funcoppc  17782  fulloppc  17831  fuccofval  17869  natpropd  17886  catccofval  18011  xpchomfval  18085  xpccofval  18088  lubfval  18254  glbfval  18267  grpidpropd  18536  gsumpropd2lem  18553  frmdplusg  18728  efmndplusg  18754  grpinvpropd  18894  grpsubpropd  18924  grpsubpropd2  18925  mulgpropd  18995  ecqusaddd  19071  oppgmnd  19233  sylow1lem2  19478  sylow3lem1  19506  prds1  20208  pwsmgp  20212  opprrng  20230  rngidpropd  20300  dvdsrpropd  20301  unitpropd  20302  invrpropd  20303  rhm1  20374  rhmopp  20394  rhmsubclem2  20571  lmhmpropd  20977  lidlrsppropd  21151  rngqiprnglinlem2  21199  lpival  21231  pzriprnglem11  21398  zrhpropd  21421  znle  21443  frlmplusgval  21671  frlmvscafval  21673  ressascl  21803  asclpropd  21804  aspval2  21805  psrbas  21840  psrplusg  21843  psrmulr  21849  psrvscafval  21855  resspsrbas  21881  ressmplbas2  21932  opsrle  21952  opsrbaslem  21954  vr1val  22074  ressply1add  22112  ressply1mul  22113  ressply1vsca  22114  psrplusgpropd  22118  mplbaspropd  22119  psropprmul  22120  ply1baspropd  22125  ply1plusgpropd  22126  ply1sca2  22136  ply1ascl0  22137  ply1ascl1  22138  subrgvr1  22145  coe1mul2lem2  22152  ply1coe1eq  22185  evls1addd  22256  evls1muld  22257  evls1vsca  22258  rhmply1vr1  22272  rhmply1vsca  22273  mamudi  22288  mamudir  22289  matrcl  22297  oftpos  22337  mattpos1  22341  mdetfval  22471  mdetrlin  22487  mdetrsca  22488  mdetrsca2  22489  mdetrlin2  22492  mdetunilem5  22501  madufval  22522  madugsum  22528  idmatidpmat  22622  cpmidpmat  22758  cncmp  23277  2ndcsep  23344  llyeq  23355  nllyeq  23356  xkouni  23484  hmphindis  23682  xkocnv  23699  ptcmplem2  23938  snclseqg  24001  prdstmdd  24009  ustexsym  24101  ucnextcn  24189  metreslem  24248  comet  24399  nrmmetd  24460  nmpropd  24480  isngp3  24484  ngpds  24490  subgnm  24519  tngnm  24537  idnghm  24629  cnmetdval  24656  cnmpopc  24820  htpyco2  24876  phtpyco2  24887  clsocv  25148  rrxprds  25287  rrxnm  25289  rrxplusgvscavalb  25293  ovolunlem1a  25395  voliunlem3  25451  ioombl1lem4  25460  uniioombllem4  25485  itg11  25590  itgeq1f  25670  itgeq1fOLD  25671  itgeq1  25672  itgeq2  25677  iblss2  25705  itgss  25711  itgeqa  25713  itgfsum  25726  itgsplit  25735  ditgeq1  25747  ditgeq2  25748  ditgeq3  25749  dvcmulf  25846  dvmptfsum  25877  dvcnvrelem2  25921  mdegfval  25965  mdegpropd  25987  deg1propd  25989  plyeq0  26114  coe11  26156  dgrlt  26170  dgradd2  26172  dgrmulc  26175  dvply1  26189  fta1lem  26213  pserulm  26329  rlimcnp2  26874  jensenlem1  26895  basellem5  26993  dchrbas  27144  dchrrcl  27149  dchrplusg  27156  dchrfi  27164  lgsdi  27243  lgseisenlem2  27285  lgsquadlem3  27291  dchrmusumlema  27402  rpvmasum2  27421  dchrisum0lema  27423  pntlemg  27507  nosupbnd2lem1  27625  lruneq  27823  addsval  27876  mulsval  28019  seqseq123d  28187  colperpexlem2  28680  axlowdimlem13  28903  uhgrvtxedgiedgb  29085  nb3grprlem1  29329  crctcshlem2  29767  wpthswwlks2on  29910  clwlknf1oclwwlkn  30032  frgrncvvdeq  30257  avril1  30411  0vfval  30554  imsval  30633  imsdval  30634  bcseqi  31068  normpythi  31090  cm0  31557  fh1  31566  pjcji  31632  opsqrlem5  32092  pjsdi2i  32105  pjclem3  32145  pjci  32148  golem1  32219  iuneq12daf  32505  iunrdx  32512  ofresid  32593  cnvprop  32646  coprprop  32649  f1od2  32671  dp2eq1  32822  dp2eq2  32823  fzto1st1  33053  gsumvsca1  33177  gsumvsca2  33178  urpropd  33181  resv1r  33286  nsgqusf1olem2  33360  oppr2idl  33432  opprqus0g  33436  ressply1evls1  33509  lindsunlem  33607  fedgmullem1  33612  fedgmullem2  33613  fedgmul  33614  fldsdrgfldext2  33645  fldextrspunlem1  33658  fldextrspunfld  33659  algextdeglem4  33703  crefeq  33828  rspectopn  33850  xrge0mulc1cn  33924  qqhval2  33965  esumeq12dvaf  34014  esumeq2  34019  esumf1o  34033  esumfzf  34052  esumss  34055  esumpfinvalf  34059  ofceq  34080  carsgclctunlem1  34301  itgeq12dv  34310  ccatmulgnn0dir  34526  breprexpnat  34618  bnj956  34759  bnj1385  34815  bnj96  34848  bnj548  34880  bnj553  34881  bnj554  34882  bnj602  34898  bnj18eq1  34910  bnj1234  34996  bnj1296  35004  bnj1318  35008  bnj1442  35032  bnj1450  35033  cvmliftlem5  35282  cvmliftlem10  35287  cvmlift2lem9  35304  cvmliftphtlem  35310  satfdm  35362  mthmpps  35575  rdgprc  35788  dfrdg2  35789  wsuceq123  35808  wlimeq12  35813  altopthsn  35955  altxpeq1  35967  altxpeq2  35968  ixpeq12dv  36210  prodeq12sdv  36212  itgeq12sdv  36213  ditgeq123dv  36215  cbvcsbdavw  36253  cbvcsbdavw2  36254  cbvrabdavw  36255  cbviundavw  36256  cbviindavw  36257  cbvopab1davw  36258  cbvopab2davw  36259  cbvopabdavw  36260  cbvmptdavw  36261  cbviotadavw  36263  cbvriotadavw  36264  cbvoprab1davw  36265  cbvoprab2davw  36266  cbvoprab3davw  36267  cbvoprab123davw  36268  cbvoprab12davw  36269  cbvoprab23davw  36270  cbvoprab13davw  36271  cbvixpdavw  36272  cbvsumdavw  36273  cbvproddavw  36274  cbvitgdavw  36275  cbvditgdavw  36276  cbvrabdavw2  36279  cbviundavw2  36280  cbviindavw2  36281  cbvmptdavw2  36282  cbvriotadavw2  36284  cbvmpodavw2  36285  cbvmpo1davw2  36286  cbvmpo2davw2  36287  cbvixpdavw2  36288  cbvsumdavw2  36289  cbvproddavw2  36290  cbvitgdavw2  36291  cbvditgdavw2  36292  ee7.2aOLD  36455  bj-sngleq  36961  bj-tageq  36970  bj-projeq  36986  bj-projval  36990  bj-1upleq  36993  bj-pr1eq  36996  bj-pr2eq  37010  bj-evaleq  37066  bj-imafv  37245  csbrecsg  37322  csbrdgg  37323  csboprabg  37324  csbmpo123  37325  finxpeq1  37380  finxpeq2  37381  csbfinxpg  37382  finxpreclem4  37388  cureq  37596  unceq  37597  uncov  37601  unccur  37603  finixpnum  37605  ptrest  37619  poimirlem3  37623  poimirlem9  37629  poimirlem15  37635  poimirlem16  37636  poimirlem26  37646  poimirlem27  37647  mbfposadd  37667  cnambfre  37668  iblabsnclem  37683  ftc1anclem1  37693  heiborlem4  37814  heiborlem6  37816  mpobi123f  38162  iineq12f  38164  mptbi12f  38166  eccnvepres  38274  xrneq1  38369  xrneq2  38372  cosseq  38423  redundss3  38625  riotaclbgBAD  38953  toycom  38972  ldualvbase  39125  ldualfvadd  39127  ldualsca  39131  ldualsbase  39132  ldualsaddN  39133  ldualfvs  39135  ldual0  39146  ldual1  39147  ldualneg  39148  cdleme19f  40307  cdleme20m  40322  cdleme21k  40337  cdleme27b  40367  cdleme31so  40378  cdleme31sn  40379  cdleme31se  40381  cdleme31se2  40382  cdleme31sc  40383  cdleme31sde  40384  cdleme31fv  40389  cdleme40v  40468  cdleme43dN  40491  cdlemeg46ngfr  40517  ltrnco4  40738  tgrpbase  40745  tgrpopr  40746  erngbase  40800  erngfplus  40801  erngfmul  40804  erngbase-rN  40808  erngfplus-rN  40809  erngfmul-rN  40812  dvasca  41005  dvavbase  41012  dvafvadd  41013  dvafvsca  41015  tendocnv  41020  dvhsca  41081  dvhfplusr  41083  dvhvbase  41086  dvhfvadd  41090  dvhfvsca  41099  lcdvadd  41596  lcdsbase  41599  lcdsadd  41600  lcdvs  41602  lcd0  41607  lcd1  41608  lcdneg  41609  fsuppind  42583  imaiinfv  42686  mapfzcons1  42710  rexrabdioph  42787  dnnumch1  43037  dnwech  43041  aomclem6  43052  pwssplit4  43082  pwfi2f1o  43089  mendplusgfval  43174  mendvscafval  43179  harval3  43531  dssmapntrcls  44121  scotteqd  44230  colleq12d  44246  uzmptshftfval  44339  dropab1  44440  dropab2  44441  iineq12dv  45104  rabbida2  45130  rabbida3  45133  itgsinexplem1  45955  wallispi2lem2  46073  fourierdlem36  46144  etransclem4  46239  fcoreslem1  47067  afveq12d  47137  aoveq123d  47182  aovfundmoveq  47185  aovnuoveq  47195  aovvoveq  47196  aovovn0oveq  47198  afv2eq12d  47219  fsumsplitsndif  47377  rngccofvalALTV  48274  rhmsubcALTVlem2  48286  ringccofvalALTV  48308  itscnhlinecirc02plem2  48788  oppfrcl3  49135  oppf1st2nd  49136  uppropd  49186  natoppf  49234  catcrcl  49400  lmdpropd  49662  cmdpropd  49663  lmddu  49672  cmddu  49673  setrecseq  49690  aacllem  49806