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

Theorem anassrs 648
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 605 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 432 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  anass  649  mpanr1  683  pm2.61ddan  792  pm2.61dda  793  anass1rs  807  anabss5  816  anabss7  821  pm2.61da2ne  2762  ralimdvva  2854  2ralbida  2884  2ralbidva  2885  2rexbidva  2960  copsexg  4722  pofun  4806  imainss  5411  eqfnfv2  5967  fnex  6124  f1elima  6156  fliftfun  6195  isores2  6214  f1oiso  6232  ovmpt2dxf  6413  grpridd  6500  sorpssuni  6574  sorpssint  6575  tfindsg2  6681  oalim  7184  omlim  7185  oaass  7212  omlimcl  7229  omass  7231  oelim2  7246  oeoa  7248  oeoelem  7249  nnaass  7273  omabs  7298  eroveu  7408  sbthlem4  7632  fimaxg  7769  fisupg  7770  fofinf1o  7803  ordtypelem7  7952  hartogs  7972  card2on  7983  unwdomg  8013  wemapwe  8142  wemapweOLD  8143  dfac5  8512  cfsmolem  8653  isf32lem2  8737  ttukeylem6  8897  ondomon  8941  alephreg  8960  ltexprlem6  9422  recexsrlem  9483  wloglei  10092  recextlem2  10187  fimaxre  10497  creur  10537  uzind3OLD  10965  uz11  11114  xrmaxeq  11391  xrmineq  11392  xaddf  11434  xaddass  11452  xleadd1a  11456  xlt2add  11463  xmullem  11467  xmulgt0  11486  xmulasslem3  11489  xlemul1a  11491  xadddilem  11497  fzrevral  11774  seqcaopr2  12125  expnlbnd2  12279  faclbnd4lem4  12356  shftlem  12883  01sqrex  13065  cau3lem  13169  limsupbnd2  13288  clim2  13309  clim2c  13310  clim0c  13312  rlimresb  13370  2clim  13377  climabs0  13390  climcn1  13396  climcn2  13397  o1rlimmul  13423  climsqz  13445  climsqz2  13446  rlimsqzlem  13453  lo1le  13456  climsup  13474  caucvgrlem2  13479  iseralt  13489  summolem2  13520  fsum2dlem  13567  cvgcmp  13612  cvgcmpce  13614  climfsum  13616  fsumiun  13617  geomulcvg  13667  mertenslem2  13676  mertens  13677  prodfn0  13685  prodfrec  13686  zprod  13726  fprodeq0  13761  fprodn0  13765  fprod2dlem  13766  smu01lem  14117  gcdcllem1  14131  gcdmultiplez  14171  dvdssq  14180  coprmdvds2  14226  pclem  14344  pcge0  14367  pcgcd1  14382  prmpwdvds  14404  1arithlem4  14426  4sqlem18  14462  vdwlem10  14490  vdwlem11  14491  ramval  14508  ramub1lem2  14527  ramcl  14529  imasaddfnlem  14907  imasaddflem  14909  imasvscafn  14916  imasleval  14920  ismon2  15111  isepi2  15118  issubc3  15197  cofucl  15236  setcmon  15393  setcepi  15394  ipodrsfi  15772  ipodrsima  15774  isacs3lem  15775  grpidpropd  15867  gsumpropd2lem  15879  mhmpropd  15951  mhmima  15973  gsumccat  15988  grplcan  16081  mulgdirlem  16145  subgmulg  16194  issubg4  16199  subgint  16204  cycsubgcl  16206  ssnmz  16222  gastacl  16326  orbsta  16330  cntzsubg  16353  galactghm  16407  odmulg  16557  odbezout  16559  sylow3lem2  16627  lsmsubm  16652  efgsfo  16736  mulgmhm  16815  mulgghm  16816  gsumval3OLD  16887  gsumval3  16890  gsumcllem  16891  gsumcllemOLD  16892  gsumpt  16967  gsumptOLD  16968  gsum2d  16978  gsum2dOLD  16979  gsum2d2  16981  prdsgsum  16986  prdsgsumOLD  16987  subgdmdprd  17060  dprd2d2  17072  ablfac1eu  17103  srglmhm  17165  srgrmhm  17166  ringpropd  17209  ringlghm  17229  dvdsrpropd  17324  abvpropd  17470  islmodd  17497  lmodprop2d  17551  lsssubg  17582  lsspropd  17642  lmhmima  17672  lsmelval2  17710  lidlsubg  17841  assapropd  17955  asclpropd  17974  psrass1lem  18008  mplcoe1  18106  mplcoe5  18110  mplcoe2OLD  18112  mplind  18146  evlslem2  18159  evlsval  18167  coe1tmmul2  18296  phlpropd  18668  frlmsslsp  18807  frlmsslspOLD  18808  lindfmm  18840  islindf4  18851  mamuass  18882  mavmulass  19029  mdetuni0  19101  mdetmul  19103  cpmatacl  19195  cpmadugsumfi  19356  cpmadugsum  19357  cpmadumatpolylem1  19360  cpmadumatpolylem2  19361  cpmadumatpoly  19362  cayhamlem4  19367  neips  19592  neindisj  19596  ordtrest2lem  19682  lmbrf  19739  lmss  19777  isreg2  19856  lmmo  19859  hauscmplem  19884  bwth  19888  2ndcomap  19937  1stcelcls  19940  restlly  19962  islly2  19963  cldllycmp  19974  comppfsc  20011  1stckgenlem  20032  txbas  20046  txbasval  20085  tx1cn  20088  ptpjopn  20091  ptcnp  20101  txnlly  20116  txlm  20127  xkococn  20139  fgabs  20358  fmfnfmlem4  20436  flimcf  20461  hauspwpwf1  20466  fclsbas  20500  fclscf  20504  flimfnfcls  20507  ghmcnp  20591  tsmsxp  20635  isxmet2d  20808  elmopn2  20926  mopni3  20975  blsscls2  20985  metequiv2  20991  metss2lem  20992  met2ndci  21003  metrest  21005  metcnp  21022  metcnp2  21023  metcnpi3  21027  txmetcnp  21028  nmolb2d  21203  xrge0tsms  21317  metdsre  21335  metnrmlem3  21343  fsumcn  21352  elcncf2  21372  mulc1cncf  21387  cncfco  21389  cncfmet  21390  bndth  21436  evth  21437  copco  21496  pcopt2  21501  pcoass  21502  pcorevlem  21504  lmmcvg  21678  lmmbrf  21679  iscau4  21696  iscauf  21697  cmetcaulem  21705  iscmet3lem3  21707  iscmet3lem1  21708  causs  21715  equivcfil  21716  lmclim  21719  caubl  21724  caublcls  21725  bcth3  21748  ivthle  21846  ivthle2  21847  ovoliunlem1  21891  ovolicc2lem5  21910  volsuplem  21943  uniioombllem6  21975  dyaddisjlem  21982  dyadmax  21985  volcn  21993  mbfmulc2lem  22032  ismbf3d  22039  mbfsup  22049  mbfinf  22050  mbflim  22053  i1fmullem  22079  itg2seq  22127  itg2uba  22128  itg2splitlem  22133  itg2split  22134  itg2monolem1  22135  ditgsplitlem  22242  ellimc2  22259  ellimc3  22261  limcflf  22263  limcmpt  22265  limcco  22275  lhop1lem  22392  dvfsumle  22400  dvfsumabs  22402  dvfsumrlim  22410  ftc1a  22416  ftc1lem6  22420  mdegmullem  22456  elply2  22571  plypf1  22587  ulmcaulem  22767  ulmcau  22768  ulmss  22770  ulmdvlem3  22775  mtest  22777  itgulm  22781  abelthlem8  22812  abelth  22814  tanord  22903  cxpcn3lem  23099  mcubic  23156  cubic2  23157  dvdsflsumcom  23442  fsumdvdsmul  23449  lgsdchrval  23600  2sqlem9  23626  rplogsumlem2  23648  rpvmasumlem  23650  dchrvmasumlem1  23658  vmalogdivsum2  23701  logsqvma  23705  selberg  23711  selberg4  23724  pntibndlem3  23755  pntlem3  23772  pntleml  23774  padicabv  23793  padicabvf  23794  padicabvcxp  23795  ostth3  23801  axpasch  24222  axcontlem7  24251  axcontlem10  24254  cusgrasize2inds  24455  2spotdisj  25039  grpolcan  25213  isgrp2d  25215  ghgrpOLD  25348  nvmul0or  25525  sspival  25629  nmosetre  25657  blocnilem  25697  blocni  25698  h2hcau  25874  h2hlm  25875  shsel3  26211  chscllem2  26534  homulcl  26656  adjsym  26730  cnvadj  26789  hhcno  26801  hhcnf  26802  lnopl  26811  unoplin  26817  counop  26818  lnfnl  26828  hmoplin  26839  hmopm  26918  nmcexi  26923  lnconi  26930  riesz3i  26959  leopmuli  27030  leopmul  27031  hstle  27127  mdsl0  27207  mdslmd1lem2  27223  atcvatlem  27282  chirredi  27291  cdj1i  27330  foresf1o  27381  isoun  27498  difioo  27571  xrge0tsmsd  27753  pstmxmet  27854  ordtrest2NEWlem  27882  dya2icoseg2  28227  eulerpartlemgc  28279  eulerpartlemgvv  28293  eulerpartlemgh  28295  eulerpartlemgs2  28297  ballotlemimin  28422  signstfvneq0  28507  conpcon  28658  cvmliftmolem2  28705  cvmliftlem6  28713  cvmliftlem8  28715  cvmlift2lem10  28735  cvmlift2lem12  28737  elmrsubrn  28858  relexpsucl  29033  relexpcnv  29034  relexpdm  29036  relexprn  29037  relexpadd  29039  relexpindlem  29040  rtrclreclem.trans  29047  rtrclreclem.min  29048  rtrclind  29050  dfon2lem6  29196  poseq  29309  nocvxminlem  29426  nofulllem5  29442  ifscgr  29670  brsegle  29734  finixpnum  30014  fin2solem  30015  fin2so  30016  heicant  30025  itg2gt0cn  30046  bddiblnc  30061  ftc1cnnc  30065  ftc1anclem5  30070  ftc1anclem6  30071  ftc1anclem7  30072  ftc1anc  30074  neibastop2lem  30154  cover2  30180  filbcmb  30207  fdc  30214  fdc1  30215  seqpo  30216  incsequz  30217  incsequz2  30218  metf1o  30224  lmclim2  30227  geomcau  30228  isbnd2  30255  bndss  30258  ismtybndlem  30278  heibor1lem  30281  rrncmslem  30304  rrnequiv  30307  exidreslem  30315  ghomco  30321  isdrngo3  30338  rngoisocnv  30360  isidlc  30388  idlnegcl  30395  divrngidl  30401  intidl  30402  unichnidl  30404  keridl  30405  igenmin  30437  prnc  30440  ispridlc  30443  prter3  30599  lsmfgcl  30996  kercvrlsm  31005  unxpwdom3  31017  hbt  31055  cntzsdrg  31127  cvgdvgrat  31170  lcmgcdlem  31188  lcmdvds  31190  climinf  31566  clim2f  31596  clim2cf  31610  clim0cf  31614  mgmhmpropd  32427  mgmhmima  32444  ovmpt2rdxf  32796  cotsqcscsq  33026  glbconxN  34977  atltcvr  35034  3dim1  35066  lvolnle3at  35181  linepsubN  35351  osumclN  35566  pexmidALTN  35577  lhpmatb  35630  cdlemg1idlemN  36173  dihlss  36852  dihglblem5aN  36894  dihatlat  36936
  Copyright terms: Public domain W3C validator