Theorem 3eqtr4g 2790

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

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

This theorem is referenced by:  rabbidva2  3410  rabbida4  3434  rabeqf  3443  csbeq1  3868  csbeq2  3870  csbeq2d  3871  csbeq2dv  3872  difeq1  4085  difeq2  4086  uneq2  4128  ineq1  4179  ineq2  4180  symdifeq1  4221  symdifeq2  4222  dfrab3ss  4289  csbprc  4375  csbnestgfw  4388  csbnestgf  4393  disjssun  4434  ifeq1  4495  ifeq2  4496  pweqALT  4581  sneq  4602  rabsneq  4611  csbsng  4675  csbprg  4676  preq1  4700  preq2  4701  tpeq1  4709  tpeq2  4710  tpeq3  4711  prprc1  4732  tpprceq3  4771  opeq1  4840  opeq2  4841  oteq1  4849  oteq2  4850  oteq3  4851  csbopg  4858  uniprg  4890  csbuni  4903  inteq  4916  iineq1  4976  iineq2  4979  iuneq12df  4985  iuneq12d  4988  dfiin2g  4999  iinrab  5036  iinin1  5046  iinxprg  5056  iununi  5066  opabbid  5175  opabbidv  5176  mpteq12da  5193  mpteq12f  5195  mpteq12dva  5196  csbmpt12  5520  xpeq1  5655  xpeq2  5662  rneq  5903  reseq1  5947  reseq2  5948  resima2  5990  resindm  6004  resmpt  6011  resmptf  6013  imaeq1  6029  imaeq2  6030  mptcnv  6115  xpdisj1  6137  xpdisj2  6138  resdisj  6145  dmpropg  6191  rnpropg  6198  cores  6225  cores2  6235  xpco  6265  predeq123  6278  csbpredg  6283  sspred  6286  predres  6315  suceqd  6402  sucprc  6413  iotaeq  6479  iotabi  6480  fntpg  6579  imain  6604  f1oprswap  6847  fveq1  6860  fveq2  6861  fvres  6880  csbfv12  6909  fnimapr  6947  fnimatpd  6948  fvco2  6961  xpprsng  7115  residpr  7118  fsnunfv  7164  fsnunres  7165  funiunfv  7225  f1ofvswap  7284  fliftf  7293  isoini2  7317  eqfunressuc  7339  riotaeqdv  7348  riotabidv  7349  riotauni  7353  riotabidva  7366  snriota  7380  oveq  7396  oveq1  7397  oveq2  7398  oprabbid  7457  oprabbidv  7458  mpoeq123  7464  mpoeq123dva  7466  mpoeq3dva  7469  resmpo  7512  ovres  7558  f1ocnvd  7643  ofeqd  7658  ofreq  7660  fpar  8098  frecseq123  8264  csbfrecsg  8266  wrecseq123  8295  csbwrecsg  8300  onovuni  8314  recseq  8345  tfr2a  8366  rdgeq1  8382  rdgeq2  8383  rdgsucmptf  8399  frsucmpt  8409  seqomeq12  8425  seqomsuc  8428  omopthi  8628  eceq1  8713  eceq2  8715  qseq1  8733  qseq2  8734  uniqs  8750  ecinxp  8768  qsinxp  8769  erovlem  8789  ecopovtrn  8796  ixpeq1  8884  unfi  9141  supeq1  9403  supeq2  9406  supeq3  9407  supeq123d  9408  infeq1  9435  infeq2  9438  infeq3  9439  infeq123d  9440  infiso  9468  oieq1  9472  oieq2  9473  ordtypelem1  9478  inf3lemc  9586  wemapwe  9657  ttrcleq  9669  r1sucg  9729  r1limg  9731  rankprb  9811  karden  9855  djueq12  9864  cardiun  9942  acneq  10003  alephlim  10027  alephsuc  10028  alephfplem2  10065  infpssrlem2  10264  fin23lem34  10306  fin23lem35  10307  zorn2lem1  10456  zorn2lem7  10462  fpwwe2lem5  10595  fpwwe2lem12  10602  addpiord  10844  mulpiord  10845  addpqnq  10898  mulpqnq  10901  addassnq  10918  mulassnq  10919  distrnq  10921  lterpq  10930  ltexnq  10935  ltsrpr  11037  00sr  11059  recexsrlem  11063  mulgt0sr  11065  addcnsrec  11103  mulcnsrec  11104  negeq  11420  csbnegg  11425  negsubdi  11485  mulneg1  11621  negfi  12139  deceq1  12661  deceq2  12662  xnegeq  13174  fseq1p1m1  13566  om2uzrdg  13928  uzrdgsuci  13932  seqeq1  13976  seqeq2  13977  seqeq3  13978  seqfeq4  14023  seqof  14031  hashprg  14367  hashtpg  14457  csbwrdg  14516  s1eq  14572  cats1co  14829  s2eqd  14836  s3eqd  14837  s4eqd  14838  s5eqd  14839  s6eqd  14840  s7eqd  14841  s8eqd  14842  xpcogend  14947  shftval  15047  limsupgle  15450  lo1eq  15541  rlimeq  15542  sumeq1  15662  sumeq2w  15665  sumeq2ii  15666  sumeq2sdv  15676  zsum  15691  sumss2  15699  fsumsplitsnun  15728  isumclim3  15732  fsumcom2  15747  incexclem  15809  incexc2  15811  isumshft  15812  prodeq1f  15879  prodeq1  15880  prodeq2w  15883  prodeq2ii  15884  prodeq2sdv  15896  zprod  15910  fprodm1s  15943  fprodp1s  15944  fprodcom2  15957  fprodsplitf  15961  iprodclim3  15973  ef0lem  16051  ruclem7  16211  sadcp1  16432  smupp1  16457  smueqlem  16467  algrp1  16551  dfphi2  16751  prmdiveq  16763  pceulem  16823  vdwlem6  16964  cshwsiun  17077  sloteq  17160  setsid  17184  elbasfv  17192  elbasov  17193  imastset  17492  imasvscaval  17508  isoval  17734  funcoppc  17844  fulloppc  17893  fuccofval  17931  natpropd  17948  catccofval  18073  xpchomfval  18147  xpccofval  18150  lubfval  18316  glbfval  18329  grpidpropd  18596  gsumpropd2lem  18613  frmdplusg  18788  efmndplusg  18814  grpinvpropd  18954  grpsubpropd  18984  grpsubpropd2  18985  mulgpropd  19055  ecqusaddd  19131  oppgmnd  19293  sylow1lem2  19536  sylow3lem1  19564  prds1  20239  pwsmgp  20243  opprrng  20261  rngidpropd  20331  dvdsrpropd  20332  unitpropd  20333  invrpropd  20334  rhm1  20405  rhmopp  20425  rhmsubclem2  20602  lmhmpropd  20987  lidlrsppropd  21161  rngqiprnglinlem2  21209  lpival  21241  pzriprnglem11  21408  zrhpropd  21431  znle  21453  frlmplusgval  21680  frlmvscafval  21682  ressascl  21812  asclpropd  21813  aspval2  21814  psrbas  21849  psrplusg  21852  psrmulr  21858  psrvscafval  21864  resspsrbas  21890  ressmplbas2  21941  opsrle  21961  opsrbaslem  21963  vr1val  22083  ressply1add  22121  ressply1mul  22122  ressply1vsca  22123  psrplusgpropd  22127  mplbaspropd  22128  psropprmul  22129  ply1baspropd  22134  ply1plusgpropd  22135  ply1sca2  22145  ply1ascl0  22146  ply1ascl1  22147  subrgvr1  22154  coe1mul2lem2  22161  ply1coe1eq  22194  evls1addd  22265  evls1muld  22266  evls1vsca  22267  rhmply1vr1  22281  rhmply1vsca  22282  mamudi  22297  mamudir  22298  matrcl  22306  oftpos  22346  mattpos1  22350  mdetfval  22480  mdetrlin  22496  mdetrsca  22497  mdetrsca2  22498  mdetrlin2  22501  mdetunilem5  22510  madufval  22531  madugsum  22537  idmatidpmat  22631  cpmidpmat  22767  cncmp  23286  2ndcsep  23353  llyeq  23364  nllyeq  23365  xkouni  23493  hmphindis  23691  xkocnv  23708  ptcmplem2  23947  snclseqg  24010  prdstmdd  24018  ustexsym  24110  ucnextcn  24198  metreslem  24257  comet  24408  nrmmetd  24469  nmpropd  24489  isngp3  24493  ngpds  24499  subgnm  24528  tngnm  24546  idnghm  24638  cnmetdval  24665  cnmpopc  24829  htpyco2  24885  phtpyco2  24896  clsocv  25157  rrxprds  25296  rrxnm  25298  rrxplusgvscavalb  25302  ovolunlem1a  25404  voliunlem3  25460  ioombl1lem4  25469  uniioombllem4  25494  itg11  25599  itgeq1f  25679  itgeq1fOLD  25680  itgeq1  25681  itgeq2  25686  iblss2  25714  itgss  25720  itgeqa  25722  itgfsum  25735  itgsplit  25744  ditgeq1  25756  ditgeq2  25757  ditgeq3  25758  dvcmulf  25855  dvmptfsum  25886  dvcnvrelem2  25930  mdegfval  25974  mdegpropd  25996  deg1propd  25998  plyeq0  26123  coe11  26165  dgrlt  26179  dgradd2  26181  dgrmulc  26184  dvply1  26198  fta1lem  26222  pserulm  26338  rlimcnp2  26883  jensenlem1  26904  basellem5  27002  dchrbas  27153  dchrrcl  27158  dchrplusg  27165  dchrfi  27173  lgsdi  27252  lgseisenlem2  27294  lgsquadlem3  27300  dchrmusumlema  27411  rpvmasum2  27430  dchrisum0lema  27432  pntlemg  27516  nosupbnd2lem1  27634  lruneq  27825  addsval  27876  mulsval  28019  seqseq123d  28187  colperpexlem2  28665  axlowdimlem13  28888  uhgrvtxedgiedgb  29070  nb3grprlem1  29314  crctcshlem2  29755  wpthswwlks2on  29898  clwlknf1oclwwlkn  30020  frgrncvvdeq  30245  avril1  30399  0vfval  30542  imsval  30621  imsdval  30622  bcseqi  31056  normpythi  31078  cm0  31545  fh1  31554  pjcji  31620  opsqrlem5  32080  pjsdi2i  32093  pjclem3  32133  pjci  32136  golem1  32207  iuneq12daf  32492  iunrdx  32499  ofresid  32573  cnvprop  32626  coprprop  32629  f1od2  32651  dp2eq1  32800  dp2eq2  32801  fzto1st1  33066  gsumvsca1  33186  gsumvsca2  33187  urpropd  33190  resv1r  33318  nsgqusf1olem2  33392  oppr2idl  33464  opprqus0g  33468  ressply1evls1  33541  lindsunlem  33627  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  fldsdrgfldext2  33665  fldextrspunlem1  33677  fldextrspunfld  33678  algextdeglem4  33717  crefeq  33842  rspectopn  33864  xrge0mulc1cn  33938  qqhval2  33979  esumeq12dvaf  34028  esumeq2  34033  esumf1o  34047  esumfzf  34066  esumss  34069  esumpfinvalf  34073  ofceq  34094  carsgclctunlem1  34315  itgeq12dv  34324  ccatmulgnn0dir  34540  breprexpnat  34632  bnj956  34773  bnj1385  34829  bnj96  34862  bnj548  34894  bnj553  34895  bnj554  34896  bnj602  34912  bnj18eq1  34924  bnj1234  35010  bnj1296  35018  bnj1318  35022  bnj1442  35046  bnj1450  35047  cvmliftlem5  35283  cvmliftlem10  35288  cvmlift2lem9  35305  cvmliftphtlem  35311  satfdm  35363  mthmpps  35576  rdgprc  35789  dfrdg2  35790  wsuceq123  35809  wlimeq12  35814  altopthsn  35956  altxpeq1  35968  altxpeq2  35969  ixpeq12dv  36211  prodeq12sdv  36213  itgeq12sdv  36214  ditgeq123dv  36216  cbvcsbdavw  36254  cbvcsbdavw2  36255  cbvrabdavw  36256  cbviundavw  36257  cbviindavw  36258  cbvopab1davw  36259  cbvopab2davw  36260  cbvopabdavw  36261  cbvmptdavw  36262  cbviotadavw  36264  cbvriotadavw  36265  cbvoprab1davw  36266  cbvoprab2davw  36267  cbvoprab3davw  36268  cbvoprab123davw  36269  cbvoprab12davw  36270  cbvoprab23davw  36271  cbvoprab13davw  36272  cbvixpdavw  36273  cbvsumdavw  36274  cbvproddavw  36275  cbvitgdavw  36276  cbvditgdavw  36277  cbvrabdavw2  36280  cbviundavw2  36281  cbviindavw2  36282  cbvmptdavw2  36283  cbvriotadavw2  36285  cbvmpodavw2  36286  cbvmpo1davw2  36287  cbvmpo2davw2  36288  cbvixpdavw2  36289  cbvsumdavw2  36290  cbvproddavw2  36291  cbvitgdavw2  36292  cbvditgdavw2  36293  ee7.2aOLD  36456  bj-sngleq  36962  bj-tageq  36971  bj-projeq  36987  bj-projval  36991  bj-1upleq  36994  bj-pr1eq  36997  bj-pr2eq  37011  bj-evaleq  37067  bj-imafv  37246  csbrecsg  37323  csbrdgg  37324  csboprabg  37325  csbmpo123  37326  finxpeq1  37381  finxpeq2  37382  csbfinxpg  37383  finxpreclem4  37389  cureq  37597  unceq  37598  uncov  37602  unccur  37604  finixpnum  37606  ptrest  37620  poimirlem3  37624  poimirlem9  37630  poimirlem15  37636  poimirlem16  37637  poimirlem26  37647  poimirlem27  37648  mbfposadd  37668  cnambfre  37669  iblabsnclem  37684  ftc1anclem1  37694  heiborlem4  37815  heiborlem6  37817  mpobi123f  38163  iineq12f  38165  mptbi12f  38167  eccnvepres  38275  xrneq1  38370  xrneq2  38373  cosseq  38424  redundss3  38626  riotaclbgBAD  38954  toycom  38973  ldualvbase  39126  ldualfvadd  39128  ldualsca  39132  ldualsbase  39133  ldualsaddN  39134  ldualfvs  39136  ldual0  39147  ldual1  39148  ldualneg  39149  cdleme19f  40309  cdleme20m  40324  cdleme21k  40339  cdleme27b  40369  cdleme31so  40380  cdleme31sn  40381  cdleme31se  40383  cdleme31se2  40384  cdleme31sc  40385  cdleme31sde  40386  cdleme31fv  40391  cdleme40v  40470  cdleme43dN  40493  cdlemeg46ngfr  40519  ltrnco4  40740  tgrpbase  40747  tgrpopr  40748  erngbase  40802  erngfplus  40803  erngfmul  40806  erngbase-rN  40810  erngfplus-rN  40811  erngfmul-rN  40814  dvasca  41007  dvavbase  41014  dvafvadd  41015  dvafvsca  41017  tendocnv  41022  dvhsca  41083  dvhfplusr  41085  dvhvbase  41088  dvhfvadd  41092  dvhfvsca  41101  lcdvadd  41598  lcdsbase  41601  lcdsadd  41602  lcdvs  41604  lcd0  41609  lcd1  41610  lcdneg  41611  fsuppind  42585  imaiinfv  42688  mapfzcons1  42712  rexrabdioph  42789  dnnumch1  43040  dnwech  43044  aomclem6  43055  pwssplit4  43085  pwfi2f1o  43092  mendplusgfval  43177  mendvscafval  43182  harval3  43534  dssmapntrcls  44124  scotteqd  44233  colleq12d  44249  uzmptshftfval  44342  dropab1  44443  dropab2  44444  iineq12dv  45107  rabbida2  45133  rabbida3  45136  itgsinexplem1  45959  wallispi2lem2  46077  fourierdlem36  46148  etransclem4  46243  fcoreslem1  47068  afveq12d  47138  aoveq123d  47183  aovfundmoveq  47186  aovnuoveq  47196  aovvoveq  47197  aovovn0oveq  47199  afv2eq12d  47220  fsumsplitsndif  47378  rngccofvalALTV  48262  rhmsubcALTVlem2  48274  ringccofvalALTV  48296  itscnhlinecirc02plem2  48776  oppfrcl3  49123  oppf1st2nd  49124  uppropd  49174  natoppf  49222  catcrcl  49388  lmdpropd  49650  cmdpropd  49651  lmddu  49660  cmddu  49661  setrecseq  49678  aacllem  49794