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

Theorem anassrs 652
Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
anassrs.1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
anassrs  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )

Proof of Theorem anassrs
StepHypRef Expression
1 anassrs.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
21exp32 608 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 433 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372
This theorem is referenced by:  anass  653  mpanr1  687  pm2.61ddan  799  pm2.61dda  800  anass1rs  814  anabss5  823  anabss7  828  pm2.61da2ne  2750  ralimdvva  2843  2ralbida  2873  2ralbidva  2874  2rexbidva  2952  copsexg  4707  pofun  4791  imainss  5271  eqfnfv2  5992  fnex  6147  f1elima  6179  fliftfun  6220  isores2  6239  f1oiso  6257  ovmpt2dxf  6436  grpridd  6523  sorpssuni  6594  sorpssint  6595  tfindsg2  6702  oalim  7242  omlim  7243  oaass  7270  omlimcl  7287  omass  7289  oelim2  7304  oeoa  7306  oeoelem  7307  nnaass  7331  omabs  7356  eroveu  7466  sbthlem4  7691  fimaxg  7824  fisupg  7825  fofinf1o  7858  ordtypelem7  8039  hartogs  8059  card2on  8069  unwdomg  8099  wemapwe  8201  dfac5  8557  cfsmolem  8698  isf32lem2  8782  ttukeylem6  8942  ondomon  8986  alephreg  9005  ltexprlem6  9465  recexsrlem  9526  wloglei  10145  recextlem2  10242  fimaxre  10551  creur  10603  uz11  11181  xrmaxeq  11474  xrmineq  11475  xaddf  11517  xaddass  11535  xleadd1a  11539  xlt2add  11546  xmullem  11550  xmulgt0  11569  xmulasslem3  11572  xlemul1a  11574  xadddilem  11580  fzrevral  11877  seqcaopr2  12246  expnlbnd2  12400  faclbnd4lem4  12478  rtrclreclem3  13102  rtrclreclem4  13103  relexpindlem  13105  rtrclind  13107  shftlem  13110  01sqrex  13292  cau3lem  13396  limsupbnd2  13524  limsupbnd2OLD  13525  clim2  13546  clim2c  13547  clim0c  13549  rlimresb  13607  2clim  13614  climabs0  13627  climcn1  13633  climcn2  13634  o1rlimmul  13660  climsqz  13682  climsqz2  13683  rlimsqzlem  13690  lo1le  13693  climsup  13711  caucvgrlem2  13718  iseralt  13729  summolem2  13760  fsum2dlem  13809  cvgcmp  13854  cvgcmpce  13856  climfsum  13858  fsumiun  13859  geomulcvg  13910  mertenslem2  13919  mertens  13920  prodfn0  13928  prodfrec  13929  zprod  13969  fprodeq0  14007  fprodn0  14011  fprod2dlem  14012  smu01lem  14433  gcdcllem1  14447  gcdmultiplez  14490  dvdssq  14499  lcmgcdlem  14536  lcmdvds  14538  coprmdvds2  14622  pclem  14742  pcge0  14765  pcgcd1  14780  prmpwdvds  14802  1arithlem4  14824  4sqlem18OLD  14860  4sqlem18  14866  vdwlem10  14894  vdwlem11  14895  ramval  14914  ramvalOLD  14915  ramub1lem2  14939  ramcl  14941  imasaddfnlem  15376  imasaddflem  15378  imasvscafn  15385  imasleval  15389  ismon2  15581  isepi2  15588  issubc3  15696  cofucl  15735  setcmon  15924  setcepi  15925  ipodrsfi  16351  ipodrsima  16353  isacs3lem  16354  grpidpropd  16446  gsumpropd2lem  16458  mhmpropd  16530  mhmima  16552  gsumccat  16567  grplcan  16660  mulgdirlem  16724  subgmulg  16773  issubg4  16778  subgint  16783  cycsubgcl  16785  ssnmz  16801  gastacl  16905  orbsta  16909  cntzsubg  16932  galactghm  16986  odmulg  17136  odbezout  17138  sylow3lem2  17206  lsmsubm  17231  efgsfo  17315  mulgmhm  17394  mulgghm  17395  gsumval3  17467  gsumcllem  17468  gsumpt  17520  gsum2d  17530  gsum2d2  17532  prdsgsum  17536  subgdmdprd  17593  dprd2d2  17603  ablfac1eu  17632  srglmhm  17694  srgrmhm  17695  ringpropd  17738  ringlghm  17758  dvdsrpropd  17850  abvpropd  17996  islmodd  18023  lmodprop2d  18076  lsssubg  18106  lsspropd  18166  lmhmima  18196  lsmelval2  18234  lidlsubg  18364  assapropd  18477  asclpropd  18496  psrass1lem  18527  mplcoe1  18615  mplcoe5  18618  mplind  18651  evlslem2  18661  evlsval  18668  coe1tmmul2  18795  phlpropd  19144  frlmsslsp  19276  lindfmm  19307  islindf4  19318  mamuass  19349  mavmulass  19496  mdetuni0  19568  mdetmul  19570  cpmatacl  19662  cpmadugsumfi  19823  cpmadugsum  19824  cpmadumatpolylem1  19827  cpmadumatpolylem2  19828  cpmadumatpoly  19829  cayhamlem4  19834  neips  20051  neindisj  20055  ordtrest2lem  20141  lmbrf  20198  lmss  20236  isreg2  20315  lmmo  20318  hauscmplem  20343  bwth  20347  2ndcomap  20395  1stcelcls  20398  restlly  20420  islly2  20421  cldllycmp  20432  comppfsc  20469  1stckgenlem  20490  txbas  20504  txbasval  20543  tx1cn  20546  ptpjopn  20549  ptcnp  20559  txnlly  20574  txlm  20585  xkococn  20597  fgabs  20816  fmfnfmlem4  20894  flimcf  20919  hauspwpwf1  20924  fclsbas  20958  fclscf  20962  flimfnfcls  20965  ghmcnp  21051  tsmsxp  21091  isxmet2d  21264  elmopn2  21382  mopni3  21431  blsscls2  21441  metequiv2  21447  metss2lem  21448  met2ndci  21459  metrest  21461  metcnp  21478  metcnp2  21479  metcnpi3  21483  txmetcnp  21484  nmolb2d  21641  xrge0tsms  21754  metdsre  21772  metnrmlem3  21780  fsumcn  21789  elcncf2  21809  mulc1cncf  21824  cncfco  21826  cncfmet  21827  bndth  21873  evth  21874  copco  21933  pcopt2  21938  pcoass  21939  pcorevlem  21941  lmmcvg  22115  lmmbrf  22116  iscau4  22133  iscauf  22134  cmetcaulem  22142  iscmet3lem3  22144  iscmet3lem1  22145  causs  22152  equivcfil  22153  lmclim  22156  caubl  22161  caublcls  22162  bcth3  22183  ivthle  22279  ivthle2  22280  ovoliunlem1  22324  ovolicc2lem5  22343  volsuplem  22376  uniioombllem6  22414  dyaddisjlem  22421  dyadmax  22424  volcn  22432  mbfmulc2lem  22471  ismbf3d  22478  mbfsup  22488  mbfinf  22489  mbfinfOLD  22490  mbflim  22494  i1fmullem  22520  itg2seq  22568  itg2uba  22569  itg2splitlem  22574  itg2split  22575  itg2monolem1  22576  ditgsplitlem  22683  ellimc2  22700  ellimc3  22702  limcflf  22704  limcmpt  22706  limcco  22716  lhop1lem  22833  dvfsumle  22841  dvfsumabs  22843  dvfsumrlim  22851  ftc1a  22857  ftc1lem6  22861  mdegmullem  22895  elply2  23009  plypf1  23025  ulmcaulem  23205  ulmcau  23206  ulmss  23208  ulmdvlem3  23213  mtest  23215  itgulm  23219  abelthlem8  23250  abelth  23252  tanord  23343  cxpcn3lem  23543  mcubic  23629  cubic2  23630  dvdsflsumcom  23971  fsumdvdsmul  23978  lgsdchrval  24129  2sqlem9  24155  rplogsumlem2  24177  rpvmasumlem  24179  dchrvmasumlem1  24187  vmalogdivsum2  24230  logsqvma  24234  selberg  24240  selberg4  24253  pntibndlem3  24284  pntlem3  24301  pntleml  24303  padicabv  24322  padicabvf  24323  padicabvcxp  24324  ostth3  24330  axpasch  24808  axcontlem7  24837  axcontlem10  24840  cusgrasize2inds  25041  2spotdisj  25625  grpolcan  25797  isgrp2d  25799  ghgrpOLD  25932  nvmul0or  26109  sspival  26213  nmosetre  26241  blocnilem  26281  blocni  26282  h2hcau  26458  h2hlm  26459  shsel3  26794  chscllem2  27117  homulcl  27238  adjsym  27312  cnvadj  27371  hhcno  27383  hhcnf  27384  lnopl  27393  unoplin  27399  counop  27400  lnfnl  27410  hmoplin  27421  hmopm  27500  nmcexi  27505  lnconi  27512  riesz3i  27541  leopmuli  27612  leopmul  27613  hstle  27709  mdsl0  27789  mdslmd1lem2  27805  atcvatlem  27864  chirredi  27873  cdj1i  27912  foresf1o  27966  isoun  28113  difioo  28191  xrge0tsmsd  28378  pstmxmet  28530  ordtrest2NEWlem  28558  esum2dlem  28743  esum2d  28744  dya2icoseg2  28930  eulerpartlemgc  29012  eulerpartlemgvv  29026  eulerpartlemgh  29028  eulerpartlemgs2  29030  ballotlemimin  29155  signstfvneq0  29240  conpcon  29737  cvmliftmolem2  29784  cvmliftlem6  29792  cvmliftlem8  29794  cvmlift2lem10  29814  cvmlift2lem12  29816  elmrsubrn  29937  dfon2lem6  30212  poseq  30269  nocvxminlem  30355  nofulllem5  30371  ifscgr  30587  brsegle  30651  neibastop2lem  30792  finixpnum  31624  fin2solem  31625  fin2so  31626  poimirlem3  31637  poimirlem4  31638  poimirlem6  31640  poimirlem7  31641  poimirlem14  31648  poimirlem16  31650  poimirlem19  31653  poimirlem22  31656  poimirlem28  31662  poimirlem29  31663  poimirlem30  31664  poimir  31667  heicant  31669  itg2gt0cn  31691  bddiblnc  31706  ftc1cnnc  31710  ftc1anclem5  31715  ftc1anclem6  31716  ftc1anclem7  31717  ftc1anc  31719  cover2  31734  filbcmb  31761  fdc  31768  fdc1  31769  seqpo  31770  incsequz  31771  incsequz2  31772  metf1o  31778  lmclim2  31781  geomcau  31782  isbnd2  31809  bndss  31812  ismtybndlem  31832  heibor1lem  31835  rrncmslem  31858  rrnequiv  31861  exidreslem  31869  ghomco  31875  isdrngo3  31892  rngoisocnv  31914  isidlc  31942  idlnegcl  31949  divrngidl  31955  intidl  31956  unichnidl  31958  keridl  31959  igenmin  31991  prnc  31994  ispridlc  31997  prter3  32152  glbconxN  32642  atltcvr  32699  3dim1  32731  lvolnle3at  32846  linepsubN  33016  osumclN  33231  pexmidALTN  33242  lhpmatb  33295  cdlemg1idlemN  33838  dihlss  34517  dihglblem5aN  34559  dihatlat  34601  lsmfgcl  35628  kercvrlsm  35637  unxpwdom3  35649  hbt  35685  cntzsdrg  35757  cvgdvgrat  36289  climinf  37246  climinfOLD  37247  clim2f  37278  clim2cf  37293  clim0cf  37297  mgmhmpropd  38533  mgmhmima  38550  ovmpt2rdxf  38870  cotsqcscsq  39233  aacllem  39291
  Copyright terms: Public domain W3C validator