MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr4g Structured version   Visualization version   GIF version

Theorem 3eqtr4g 2881
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
StepHypRef Expression
1 3eqtr4g.2 . . 3 𝐶 = 𝐴
2 3eqtr4g.1 . . 3 (𝜑𝐴 = 𝐵)
31, 2syl5eq 2868 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4g.3 . 2 𝐷 = 𝐵
53, 4syl6eqr 2874 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814
This theorem is referenced by:  rabbidva2  3477  rabeqf  3482  rabeqi  3483  csbeq1  3885  csbeq2  3887  csbeq2d  3888  difeq1  4091  difeq2  4092  uneq2  4132  ineq1  4180  ineq2  4182  symdifeq1  4220  symdifeq2  4221  dfrab3ss  4280  csbprc  4357  csbnestgfw  4370  csbnestgf  4375  disjssun  4415  ifeq1  4469  ifeq2  4470  pweq  4540  sneq  4569  csbsng  4638  csbprg  4639  preq1  4663  preq2  4664  tpeq1  4672  tpeq2  4673  tpeq3  4674  prprc1  4695  tpprceq3  4731  opeq1  4797  opeq2  4798  oteq1  4806  oteq2  4807  oteq3  4808  csbopg  4815  unieq  4840  csbuni  4860  inteq  4872  iineq1  4928  iineq2  4931  iuneq12df  4937  dfiin2g  4949  iinrab  4983  iinin1  4993  iinxprg  5003  iununi  5013  opabbid  5123  mpteq12df  5140  mpteq12f  5141  csbmpt12  5436  xpeq1  5563  xpeq2  5570  rneq  5800  reseq1  5841  reseq2  5842  resima2  5882  resindm  5894  resmpt  5899  resmptf  5901  imaeq1  5918  imaeq2  5919  mptcnv  5992  xpdisj1  6012  xpdisj2  6013  resdisj  6020  dmpropg  6066  rnpropg  6073  cores  6096  cores2  6106  xpco  6134  predeq123  6143  sspred  6150  suceq  6250  sucprc  6260  iotaeq  6320  iotabi  6321  fntpg  6408  imain  6433  f1oprswap  6652  fveq1  6663  fveq2  6664  fvres  6683  csbfv12  6707  fnimapr  6741  fvco2  6752  xpprsng  6895  residpr  6898  fsnunfv  6942  fsnunres  6943  funiunfv  6998  fliftf  7057  isoini2  7081  riotaeqdv  7104  riotabidv  7105  riotauni  7109  riotabidva  7122  snriota  7136  oveq  7151  oveq1  7152  oveq2  7153  oprabbid  7208  mpoeq123  7215  mpoeq123dva  7217  mpoeq3dva  7220  resmpo  7261  ovres  7303  f1ocnvd  7385  ofeq  7400  ofreq  7401  fpar  7802  wrecseq123  7939  onovuni  7970  recseq  8001  tfr2a  8022  rdgeq1  8038  rdgeq2  8039  rdgsucmptf  8055  frsucmpt  8064  seqomeq12  8081  seqomsuc  8084  omopthi  8274  eceq1  8317  eceq2  8319  qseq1  8333  qseq2  8334  uniqs  8347  ecinxp  8362  qsinxp  8363  erovlem  8383  ecopovtrn  8390  ixpeq1  8461  supeq1  8898  supeq2  8901  supeq3  8902  supeq123d  8903  infeq1  8929  infeq2  8932  infeq3  8933  infeq123d  8934  infiso  8961  oieq1  8965  oieq2  8966  ordtypelem1  8971  inf3lemc  9078  wemapwe  9149  r1sucg  9187  r1limg  9189  rankprb  9269  karden  9313  djueq12  9322  cardiun  9400  acneq  9458  alephlim  9482  alephsuc  9483  alephfplem2  9520  infpssrlem2  9715  fin23lem34  9757  fin23lem35  9758  zorn2lem1  9907  zorn2lem7  9913  fpwwe2lem6  10046  fpwwe2lem13  10053  addpiord  10295  mulpiord  10296  addpqnq  10349  mulpqnq  10352  addassnq  10369  mulassnq  10370  distrnq  10372  lterpq  10381  ltexnq  10386  ltsrpr  10488  00sr  10510  recexsrlem  10514  mulgt0sr  10516  addcnsrec  10554  mulcnsrec  10555  negeq  10867  csbnegg  10872  negsubdi  10931  mulneg1  11065  negfi  11578  deceq1  12092  deceq2  12093  xnegeq  12590  fseq1p1m1  12971  om2uzrdg  13314  uzrdgsuci  13318  seqeq1  13362  seqeq2  13363  seqeq3  13364  seqfeq4  13409  seqof  13417  hashprg  13746  hashtpg  13833  csbwrdg  13885  s1eq  13944  cats1co  14208  s2eqd  14215  s3eqd  14216  s4eqd  14217  s5eqd  14218  s6eqd  14219  s7eqd  14220  s8eqd  14221  xpcogend  14324  shftval  14423  limsupgle  14824  lo1eq  14915  rlimeq  14916  sumeq1  15035  sumeq2w  15039  sumeq2ii  15040  zsum  15065  sumss2  15073  fsumsplitsnun  15100  isumclim3  15104  fsumcom2  15119  incexclem  15181  incexc2  15183  isumshft  15184  prodeq1f  15252  prodeq2w  15256  prodeq2ii  15257  zprod  15281  fprodm1s  15314  fprodp1s  15315  fprodcom2  15328  fprodsplitf  15332  iprodclim3  15344  ef0lem  15422  ruclem7  15579  sadcp1  15794  smupp1  15819  smueqlem  15829  algrp1  15908  dfphi2  16101  prmdiveq  16113  pceulem  16172  vdwlem6  16312  cshwsiun  16423  sloteq  16478  setsid  16528  elbasfv  16534  elbasov  16535  imastset  16785  imasvscaval  16801  isoval  17025  funcoppc  17135  fulloppc  17182  fuccofval  17219  natpropd  17236  catccofval  17350  xpchomfval  17419  xpccofval  17422  lubfval  17578  glbfval  17591  grpidpropd  17862  gsumpropd2lem  17879  frmdplusg  18009  grpinvpropd  18114  grpsubpropd  18144  grpsubpropd2  18145  mulgpropd  18209  oppgmnd  18422  symgplusg  18447  sylow1lem2  18655  sylow3lem1  18683  prds1  19295  pwsmgp  19299  opprring  19312  rngidpropd  19376  dvdsrpropd  19377  unitpropd  19378  invrpropd  19379  rhm1  19413  lmhmpropd  19776  lidlrsppropd  19933  lpival  19948  ressascl  20055  asclpropd  20056  aspval2  20057  psrbas  20088  psrplusg  20091  psrmulr  20094  psrvscafval  20100  resspsrbas  20125  ressmplbas2  20166  opsrle  20186  opsrbaslem  20188  vr1val  20290  ressply1add  20328  ressply1mul  20329  ressply1vsca  20330  psrplusgpropd  20334  mplbaspropd  20335  psropprmul  20336  ply1baspropd  20341  ply1plusgpropd  20342  ply1sca2  20352  subrgvr1  20359  coe1mul2lem2  20366  ply1coe1eq  20396  zrhpropd  20592  znle  20613  frlmplusgval  20838  frlmvscafval  20840  mamudi  20942  mamudir  20943  matrcl  20951  oftpos  20991  mattpos1  20995  mdetfval  21125  mdetrlin  21141  mdetrsca  21142  mdetrsca2  21143  mdetrlin2  21146  mdetunilem5  21155  madufval  21176  madugsum  21182  idmatidpmat  21275  cpmidpmat  21411  cncmp  21930  2ndcsep  21997  llyeq  22008  nllyeq  22009  xkouni  22137  hmphindis  22335  xkocnv  22352  ptcmplem2  22591  snclseqg  22653  prdstmdd  22661  ustexsym  22753  ucnextcn  22842  metreslem  22901  comet  23052  nrmmetd  23113  nmpropd  23132  isngp3  23136  ngpds  23142  subgnm  23171  tngnm  23189  idnghm  23281  cnmetdval  23308  cnmpopc  23461  htpyco2  23512  phtpyco2  23523  clsocv  23782  rrxprds  23921  rrxnm  23923  rrxplusgvscavalb  23927  ovolunlem1a  24026  voliunlem3  24082  ioombl1lem4  24091  uniioombllem4  24116  itg11  24221  itgeq1f  24301  itgeq2  24307  iblss2  24335  itgss  24341  itgeqa  24343  itgfsum  24356  itgsplit  24365  ditgeq1  24375  ditgeq2  24376  ditgeq3  24377  dvcmulf  24471  dvmptfsum  24501  dvcnvrelem2  24544  mdegfval  24585  mdegpropd  24607  deg1propd  24609  plyeq0  24730  coe11  24772  dgrlt  24785  dgradd2  24787  dgrmulc  24790  dvply1  24802  fta1lem  24825  pserulm  24939  rlimcnp2  25472  jensenlem1  25492  basellem5  25590  dchrbas  25739  dchrrcl  25744  dchrplusg  25751  dchrfi  25759  lgsdi  25838  lgseisenlem2  25880  lgsquadlem3  25886  dchrmusumlema  25997  rpvmasum2  26016  dchrisum0lema  26018  pntlemg  26102  colperpexlem2  26445  axlowdimlem13  26668  uhgrvtxedgiedgb  26849  nb3grprlem1  27090  crctcshlem2  27524  wpthswwlks2on  27668  clwlknf1oclwwlkn  27791  frgrncvvdeq  28016  avril1  28170  0vfval  28311  imsval  28390  imsdval  28391  bcseqi  28825  normpythi  28847  cm0  29314  fh1  29323  pjcji  29389  opsqrlem5  29849  pjsdi2i  29862  pjclem3  29902  pjci  29905  golem1  29976  iuneq12daf  30237  iunrdx  30244  ofresid  30318  fnimatp  30352  cnvprop  30359  coprprop  30362  f1od2  30384  dp2eq1  30477  dp2eq2  30478  fzto1st1  30672  gsumvsca1  30782  gsumvsca2  30783  rhmopp  30820  resv1r  30838  lindsunlem  30920  fedgmullem1  30925  fedgmullem2  30926  fedgmul  30927  crefeq  31009  xrge0mulc1cn  31084  qqhval2  31123  esumeq12dvaf  31190  esumeq2  31195  esumf1o  31209  esumfzf  31228  esumss  31231  esumpfinvalf  31235  ofceq  31256  carsgclctunlem1  31475  itgeq12dv  31484  ccatmulgnn0dir  31712  breprexpnat  31805  bnj956  31948  bnj1385  32004  bnj96  32037  bnj548  32069  bnj553  32070  bnj554  32071  bnj602  32087  bnj18eq1  32099  bnj1234  32183  bnj1296  32191  bnj1318  32195  bnj1442  32219  bnj1450  32220  cvmliftlem5  32434  cvmliftlem10  32439  cvmlift2lem9  32456  cvmliftphtlem  32462  satfdm  32514  mthmpps  32727  eqfunressuc  32903  rdgprc  32937  dfrdg2  32938  trpredeq1  32957  trpredeq2  32958  trpredeq3  32959  wsuceq123  32999  wlimeq12  33004  frecseq123  33017  nosupbnd2lem1  33113  altopthsn  33320  altxpeq1  33332  altxpeq2  33333  ee7.2aOLD  33707  bj-rabbida2  34135  bj-sngleq  34177  bj-tageq  34186  bj-projeq  34202  bj-projval  34206  bj-1upleq  34209  bj-pr1eq  34212  bj-pr2eq  34226  bj-evaleq  34258  bj-imafv  34426  bj-isrvec  34464  csbpredg  34490  csbwrecsg  34491  csbrecsg  34492  csbrdgg  34493  csboprabg  34494  csbmpo123  34495  finxpeq1  34550  finxpeq2  34551  csbfinxpg  34552  finxpreclem4  34558  cureq  34750  unceq  34751  uncov  34755  unccur  34757  finixpnum  34759  ptrest  34773  poimirlem3  34777  poimirlem9  34783  poimirlem15  34789  poimirlem16  34790  poimirlem26  34800  poimirlem27  34801  mbfposadd  34821  cnambfre  34822  iblabsnclem  34837  ftc1anclem1  34849  heiborlem4  34975  heiborlem6  34977  mpobi123f  35323  iineq12f  35325  mptbi12f  35327  eccnvepres  35420  uniqsALTV  35469  xrneq1  35511  xrneq2  35514  cosseq  35553  redundss3  35745  riotaclbgBAD  35972  toycom  35991  ldualvbase  36144  ldualfvadd  36146  ldualsca  36150  ldualsbase  36151  ldualsaddN  36152  ldualfvs  36154  ldual0  36165  ldual1  36166  ldualneg  36167  cdleme19f  37326  cdleme20m  37341  cdleme21k  37356  cdleme27b  37386  cdleme31so  37397  cdleme31sn  37398  cdleme31se  37400  cdleme31se2  37401  cdleme31sc  37402  cdleme31sde  37403  cdleme31fv  37408  cdleme40v  37487  cdleme43dN  37510  cdlemeg46ngfr  37536  ltrnco4  37757  tgrpbase  37764  tgrpopr  37765  erngbase  37819  erngfplus  37820  erngfmul  37823  erngbase-rN  37827  erngfplus-rN  37828  erngfmul-rN  37831  dvasca  38024  dvavbase  38031  dvafvadd  38032  dvafvsca  38034  tendocnv  38039  dvhsca  38100  dvhfplusr  38102  dvhvbase  38105  dvhfvadd  38109  dvhfvsca  38118  lcdvadd  38615  lcdsbase  38618  lcdsadd  38619  lcdvs  38621  lcd0  38626  lcd1  38627  lcdneg  38628  prjspnval2  39147  imaiinfv  39170  mapfzcons1  39194  rexrabdioph  39271  dnnumch1  39524  dnwech  39528  aomclem6  39539  pwssplit4  39569  pwfi2f1o  39576  mendplusgfval  39665  mendvscafval  39670  harval3  39784  dssmapntrcls  40358  scotteqd  40453  colleq12d  40469  uzmptshftfval  40558  dropab1  40659  dropab2  40660  rabbida2  41279  rabbida3  41282  itgsinexplem1  42119  wallispi2lem2  42238  fourierdlem36  42309  etransclem4  42404  afveq12d  43213  aoveq123d  43258  aovfundmoveq  43261  aovnuoveq  43271  aovvoveq  43272  aovovn0oveq  43274  afv2eq12d  43295  fsumsplitsndif  43414  efmndplusg  43948  rngccofvalALTV  44156  ringccofvalALTV  44219  rhmsubclem2  44256  rhmsubcALTVlem2  44274  itscnhlinecirc02plem2  44668  setrecseq  44686  aacllem  44800
  Copyright terms: Public domain W3C validator