MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr4a Unicode version

Theorem 3eqtr4a 2524
Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4a.1
3eqtr4a.2
3eqtr4a.3
Assertion
Ref Expression
3eqtr4a

Proof of Theorem 3eqtr4a
StepHypRef Expression
1 3eqtr4a.2 . . 3
2 3eqtr4a.1 . . 3
31, 2syl6eq 2514 . 2
4 3eqtr4a.3 . 2
53, 4eqtr4d 2501 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395
This theorem is referenced by:  rabsnif  4099  uniintsn  4324  iinvdif  4402  iununi  4415  unizlim  4999  dmxpid  5227  rnxpid  5445  csbrn  5473  dmsnsnsn  5491  opswap  5500  xpcoid  5553  fvco4i  5951  fndmdifcom  5992  fmptsng  6092  fmptsnd  6093  csbov  6331  ordunisuc  6667  offres  6795  1stval2  6817  2ndval2  6818  cnvf1olem  6898  fparlem3  6902  fparlem4  6903  imacosupp  6959  seqomlem1  7134  ecovcom  7436  ecovass  7437  ecovdi  7438  resixpfo  7527  mapunen  7706  cardidm  8361  cardiun  8384  alephcard  8472  cardalephex  8492  cardcf  8653  cfidm  8676  alephsing  8677  itunisuc  8820  itunitc  8822  ituniiun  8823  alephadd  8973  alephreg  8978  pwcfsdom  8979  addcompq  9349  addcomnq  9350  mulcompq  9351  mulcomnq  9352  addassnq  9357  mulassnq  9358  addid1  9781  zeo  10973  xnegneg  11442  xaddcom  11466  xaddid1  11467  xnegdi  11469  xmulid1  11500  xadddilem  11515  ixxin  11575  fzsuc2  11766  expneg  12174  sq01  12288  facp1  12358  bcpasc  12399  hashf1lem1  12504  hashf1  12506  eqs1  12621  swrdccatin1  12708  swrdccat3blem  12720  repswsymballbi  12752  cshwmodn  12766  repswcshw  12780  absexp  13137  sqreulem  13192  fsumf1o  13545  fsumadd  13561  fsumrev2  13597  fsumparts  13620  fsumrelem  13621  fprodf1o  13753  fprodmul  13765  fproddiv  13766  fprodfac  13777  efexp  13836  tanval2  13868  sqr2irrlem  13981  sadeq  14122  smumullem  14142  smumul  14143  gcdcom  14158  gcd0id  14161  gcdass  14183  nn0gcdsq  14285  dfphi2  14304  pcneg  14397  setscom  14662  strfvi  14672  setsnid  14674  ressbas  14687  ressinbas  14693  ressress  14694  firest  14830  topnval  14832  xpsfeq  14961  xpsaddlem  14972  xpsvsca  14976  homffval  15086  oppchomfval  15109  oppcbas  15113  rescbas  15198  rescco  15201  cofuass  15258  fucbas  15329  fuchom  15330  setccatid  15411  xpcbas  15447  xpchomfval  15448  xpccofval  15451  oduleval  15761  oduglb  15769  odulub  15771  ipotset  15787  grpinvfvi  16091  cntrval  16357  cntzval  16359  oppgplusfval  16383  symgbas  16405  symggrp  16425  pmtrprfval  16512  m1expaddsub  16523  sylow1lem2  16619  sylow3lem1  16647  oppglsm  16662  gsumzsplit  16944  gsumzsplitOLD  16945  gsum2dlem2  16998  gsum2dOLD  17000  gsumcom2  17003  dprd2dlem2  17089  dprd2da  17091  dmdprdsplit2lem  17094  mgpplusg  17145  mgpress  17152  ringidval  17155  opprmulfval  17274  abvtrivd  17489  sralem  17823  srasca  17827  sravsca  17828  sraip  17829  rlmval  17837  psrmulr  18037  mplmonmul  18126  mplcoe3  18128  mplcoe3OLD  18129  opsrbaslem  18142  opsrtoslem2  18149  psr1val  18225  ply1basfvi  18282  ply1plusgfvi  18283  psr1sca2  18292  evl1fval1lem  18366  zlmlem  18554  zlmsca  18558  zlmvsca  18559  psgninv  18618  ocvval  18698  thlbas  18727  thlle  18728  thloc  18730  dsmmval2  18767  mattpos1  18958  mdettpos  19113  smadiadetglem1  19173  tgdif0  19494  indislem  19501  restco  19665  txtopon  20092  txindislem  20134  qtopres  20199  hmphindis  20298  ptuncnv  20308  snclseqg  20614  tsmssplit  20654  ussval  20762  tuslem  20770  setsmsbas  20978  tnglem  21154  tngds  21162  tngtset  21163  pcoass  21524  cphsqrtcl2  21633  rrxcph  21824  ovolunlem1a  21907  ioorinv  21985  itg11  22098  itg1mulc  22111  itg2cnlem1  22168  iblss2  22212  ibladdlem  22226  itgfsum  22233  iblabslem  22234  iblabs  22235  ditgneg  22261  deg1fvi  22485  dgrco  22672  logfac  22985  cxpexp  23049  cxpmul2  23070  cxpsqrt  23084  dvcxp1  23116  dvcxp2  23117  ang180lem1  23141  mcubic  23178  quart1  23187  reasinsin  23227  atanlogaddlem  23244  atantayl2  23269  log2tlbnd  23276  basellem2  23355  basellem3  23356  basellem5  23358  basellem8  23361  dchrmulid2  23527  bcp1ctr  23554  lgsneg  23594  lgsneg1  23595  lgsdir2  23603  lgsdir  23605  lgsdi  23607  lgsquad2lem2  23634  pntleml  23796  motgrp  23930  lmiisolem  24161  ttglem  24179  eupath2lem3  24979  bafval  25497  ipidsq  25623  ipasslem1  25746  pjclem2  27115  cvmdi  27243  imadifxp  27458  iundisjcnt  27603  resvsca  27820  indval2  28028  bayesth  28378  plymulx  28505  subfacp1lem6  28629  mvtval  28860  mexval  28862  mexval2  28863  mdvval  28864  mrsubfval  28868  mrsubvrs  28882  msubfval  28884  elmsubrn  28888  mvhfval  28893  mpstval  28895  msrfval  28897  mstaval  28904  mthmval  28935  fallfacfwd  29158  dfrdg2  29228  dfrdg3  29229  dfrdg4  29600  ordtoplem  29900  ordcmp  29912  mblfinlem2  30052  itg2addnclem2  30067  ibladdnclem  30071  iblabsnclem  30078  iblabsnc  30079  iblmulc2nc  30080  ftc1anclem8  30097  kelac2  31011  mendbas  31133  mendsca  31138  mendring  31141  lcmcom  31199  lcmneg  31209  lcmass  31218  iotain  31324  addrcom  31384  itgsinexplem1  31752  volioc  31771  dirkertrigeqlem1  31880  fourierdlem104  31993  sqwvfoura  32011  sqwvfourb  32012  estrccatid  32638  rngccatidOLD  32797  ringccatidOLD  32860  dpfrac1  33166  pmodN  35574  tgrpgrplem  36475  tendoplass  36509  tendoicl  36522  erngdvlem3  36716  dvhvaddass  36824  dib0  36891  dib1dim2  36895  diclspsn  36921  cdlemn8  36931  dihopelvalcpre  36975  djhcom  37132
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449
  Copyright terms: Public domain W3C validator