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  2684  ralimdvva  2771  2ralbida  2801  2ralbidva  2802  2rexbidva  2879  copsexg  4644  pofun  4728  imainss  5208  eqfnfv2  5931  fnex  6086  f1elima  6118  fliftfun  6159  isores2  6178  f1oiso  6196  ovmpt2dxf  6375  grpridd  6462  sorpssuni  6533  sorpssint  6534  tfindsg2  6641  oalim  7184  omlim  7185  oaass  7212  omlimcl  7229  omass  7231  oelim2  7246  oeoa  7248  oeoelem  7249  nnaass  7273  omabs  7298  eroveu  7408  sbthlem4  7633  fimaxg  7766  fisupg  7767  fofinf1o  7800  fiming  7962  fiinfg  7963  ordtypelem7  7987  hartogs  8007  card2on  8017  unwdomg  8047  wemapwe  8149  dfac5  8505  cfsmolem  8646  isf32lem2  8730  ttukeylem6  8890  ondomon  8934  alephreg  8953  ltexprlem6  9412  recexsrlem  9473  wloglei  10092  recextlem2  10189  fimaxre  10497  creur  10549  uz11  11127  xrmaxeq  11420  xrmineq  11421  xaddf  11463  xaddass  11481  xleadd1a  11485  xlt2add  11492  xmullem  11496  xmulgt0  11515  xmulasslem3  11518  xlemul1a  11520  xadddilem  11526  fzrevral  11825  seqcaopr2  12194  expnlbnd2  12348  faclbnd4lem4  12426  rtrclreclem3  13062  rtrclreclem4  13063  relexpindlem  13065  rtrclind  13067  shftlem  13070  01sqrex  13252  cau3lem  13356  limsupbnd2  13484  limsupbnd2OLD  13485  clim2  13506  clim2c  13507  clim0c  13509  rlimresb  13567  2clim  13574  climabs0  13587  climcn1  13593  climcn2  13594  o1rlimmul  13620  climsqz  13642  climsqz2  13643  rlimsqzlem  13650  lo1le  13653  climsup  13671  caucvgrlem2  13678  iseralt  13689  summolem2  13720  fsum2dlem  13769  cvgcmp  13814  cvgcmpce  13816  climfsum  13818  fsumiun  13819  geomulcvg  13870  mertenslem2  13879  mertens  13880  prodfn0  13888  prodfrec  13889  zprod  13929  fprodeq0  13967  fprodn0  13971  fprod2dlem  13972  smu01lem  14397  gcdcllem1  14411  gcdmultiplez  14457  dvdssq  14466  lcmgcdlem  14509  lcmdvds  14511  coprmdvds2  14598  pclem  14726  pcge0  14749  pcgcd1  14764  prmpwdvds  14786  1arithlem4  14808  4sqlem18OLD  14844  4sqlem18  14850  vdwlem10  14878  vdwlem11  14879  ramval  14898  ramvalOLD  14899  ramub1lem2  14923  ramcl  14925  imasaddfnlem  15372  imasaddflem  15374  imasvscafn  15381  imasleval  15385  ismon2  15577  isepi2  15584  issubc3  15692  cofucl  15731  setcmon  15920  setcepi  15921  ipodrsfi  16347  ipodrsima  16349  isacs3lem  16350  grpidpropd  16442  gsumpropd2lem  16454  mhmpropd  16526  mhmima  16548  gsumccat  16563  grplcan  16656  mulgdirlem  16720  subgmulg  16769  issubg4  16774  subgint  16779  cycsubgcl  16781  ssnmz  16797  gastacl  16901  orbsta  16905  cntzsubg  16928  galactghm  16982  odmulg  17145  odbezout  17147  sylow3lem2  17218  lsmsubm  17243  efgsfo  17327  mulgmhm  17406  mulgghm  17407  gsumval3  17479  gsumcllem  17480  gsumpt  17532  gsum2d  17542  gsum2d2  17544  prdsgsum  17548  subgdmdprd  17605  dprd2d2  17615  ablfac1eu  17644  srglmhm  17706  srgrmhm  17707  ringpropd  17750  ringlghm  17770  dvdsrpropd  17862  abvpropd  18008  islmodd  18035  lmodprop2d  18088  lsssubg  18118  lsspropd  18178  lmhmima  18208  lsmelval2  18246  lidlsubg  18376  assapropd  18489  asclpropd  18508  psrass1lem  18539  mplcoe1  18627  mplcoe5  18630  mplind  18663  evlslem2  18673  evlsval  18680  coe1tmmul2  18807  phlpropd  19159  frlmsslsp  19291  lindfmm  19322  islindf4  19333  mamuass  19364  mavmulass  19511  mdetuni0  19583  mdetmul  19585  cpmatacl  19677  cpmadugsumfi  19838  cpmadugsum  19839  cpmadumatpolylem1  19842  cpmadumatpolylem2  19843  cpmadumatpoly  19844  cayhamlem4  19849  neips  20066  neindisj  20070  ordtrest2lem  20156  lmbrf  20213  lmss  20251  isreg2  20330  lmmo  20333  hauscmplem  20358  bwth  20362  2ndcomap  20410  1stcelcls  20413  restlly  20435  islly2  20436  cldllycmp  20447  comppfsc  20484  1stckgenlem  20505  txbas  20519  txbasval  20558  tx1cn  20561  ptpjopn  20564  ptcnp  20574  txnlly  20589  txlm  20600  xkococn  20612  fgabs  20831  fmfnfmlem4  20909  flimcf  20934  hauspwpwf1  20939  fclsbas  20973  fclscf  20977  flimfnfcls  20980  ghmcnp  21066  tsmsxp  21106  isxmet2d  21279  elmopn2  21397  mopni3  21446  blsscls2  21456  metequiv2  21462  metss2lem  21463  met2ndci  21474  metrest  21476  metcnp  21493  metcnp2  21494  metcnpi3  21498  txmetcnp  21499  nmolb2d  21660  xrge0tsms  21789  metdsre  21807  metnrmlem3  21815  metdsreOLD  21822  metnrmlem3OLD  21830  fsumcn  21839  elcncf2  21859  mulc1cncf  21874  cncfco  21876  cncfmet  21877  bndth  21923  evth  21924  copco  21986  pcopt2  21991  pcoass  21992  pcorevlem  21994  lmmcvg  22168  lmmbrf  22169  iscau4  22186  iscauf  22187  cmetcaulem  22195  iscmet3lem3  22197  iscmet3lem1  22198  causs  22205  equivcfil  22206  lmclim  22209  caubl  22214  caublcls  22215  bcth3  22236  ivthle  22344  ivthle2  22345  ovoliunlem1  22392  ovolicc2lem5  22412  volsuplem  22445  uniioombllem6  22483  dyaddisjlem  22490  dyadmax  22493  volcn  22501  mbfmulc2lem  22540  ismbf3d  22547  mbfsup  22557  mbfinf  22558  mbfinfOLD  22559  mbflim  22563  i1fmullem  22589  itg2seq  22637  itg2uba  22638  itg2splitlem  22643  itg2split  22644  itg2monolem1  22645  ditgsplitlem  22752  ellimc2  22769  ellimc3  22771  limcflf  22773  limcmpt  22775  limcco  22785  lhop1lem  22902  dvfsumle  22910  dvfsumabs  22912  dvfsumrlim  22920  ftc1a  22926  ftc1lem6  22930  mdegmullem  22964  elply2  23087  plypf1  23103  ulmcaulem  23286  ulmcau  23287  ulmss  23289  ulmdvlem3  23294  mtest  23296  itgulm  23300  abelthlem8  23331  abelth  23333  tanord  23424  cxpcn3lem  23624  mcubic  23710  cubic2  23711  dvdsflsumcom  24054  fsumdvdsmul  24061  lgsdchrval  24212  2sqlem9  24238  rplogsumlem2  24260  rpvmasumlem  24262  dchrvmasumlem1  24270  vmalogdivsum2  24313  logsqvma  24317  selberg  24323  selberg4  24336  pntibndlem3  24367  pntlem3  24384  pntleml  24386  padicabv  24405  padicabvf  24406  padicabvcxp  24407  ostth3  24413  axpasch  24908  axcontlem7  24937  axcontlem10  24940  cusgrasize2inds  25142  2spotdisj  25726  grpolcan  25898  isgrp2d  25900  ghgrpOLD  26033  nvmul0or  26210  sspival  26314  nmosetre  26342  blocnilem  26382  blocni  26383  h2hcau  26569  h2hlm  26570  shsel3  26905  chscllem2  27228  homulcl  27349  adjsym  27423  cnvadj  27482  hhcno  27494  hhcnf  27495  lnopl  27504  unoplin  27510  counop  27511  lnfnl  27521  hmoplin  27532  hmopm  27611  nmcexi  27616  lnconi  27623  riesz3i  27652  leopmuli  27723  leopmul  27724  hstle  27820  mdsl0  27900  mdslmd1lem2  27916  atcvatlem  27975  chirredi  27984  cdj1i  28023  foresf1o  28077  isoun  28223  difioo  28309  xrge0tsmsd  28495  pstmxmet  28647  ordtrest2NEWlem  28675  esum2dlem  28860  esum2d  28861  dya2icoseg2  29047  eulerpartlemgc  29142  eulerpartlemgvv  29156  eulerpartlemgh  29158  eulerpartlemgs2  29160  ballotlemimin  29285  ballotlemiminOLD  29323  signstfvneq0  29408  conpcon  29905  cvmliftmolem2  29952  cvmliftlem6  29960  cvmliftlem8  29962  cvmlift2lem10  29982  cvmlift2lem12  29984  elmrsubrn  30105  dfon2lem6  30380  poseq  30437  nocvxminlem  30523  nofulllem5  30539  ifscgr  30755  brsegle  30819  neibastop2lem  30960  finixpnum  31837  fin2solem  31838  fin2so  31839  poimirlem3  31850  poimirlem4  31851  poimirlem6  31853  poimirlem7  31854  poimirlem14  31861  poimirlem16  31863  poimirlem19  31866  poimirlem22  31869  poimirlem28  31875  poimirlem29  31876  poimirlem30  31877  poimir  31880  heicant  31882  itg2gt0cn  31904  bddiblnc  31919  ftc1cnnc  31923  ftc1anclem5  31928  ftc1anclem6  31929  ftc1anclem7  31930  ftc1anc  31932  cover2  31947  filbcmb  31974  fdc  31981  fdc1  31982  seqpo  31983  incsequz  31984  incsequz2  31985  metf1o  31991  lmclim2  31994  geomcau  31995  isbnd2  32022  bndss  32025  ismtybndlem  32045  heibor1lem  32048  rrncmslem  32071  rrnequiv  32074  exidreslem  32082  ghomco  32088  isdrngo3  32105  rngoisocnv  32127  isidlc  32155  idlnegcl  32162  divrngidl  32168  intidl  32169  unichnidl  32171  keridl  32172  igenmin  32204  prnc  32207  ispridlc  32210  prter3  32365  glbconxN  32855  atltcvr  32912  3dim1  32944  lvolnle3at  33059  linepsubN  33229  osumclN  33444  pexmidALTN  33455  lhpmatb  33508  cdlemg1idlemN  34051  dihlss  34730  dihglblem5aN  34772  dihatlat  34814  lsmfgcl  35845  kercvrlsm  35854  unxpwdom3  35866  hbt  35902  cntzsdrg  35981  cvgdvgrat  36575  climinf  37567  climinfOLD  37568  clim2f  37599  clim2cf  37614  clim0cf  37618  cusgrsize2inds  39242  mgmhmpropd  39376  mgmhmima  39393  ovmpt2rdxf  39713  cotsqcscsq  40075  aacllem  40133
  Copyright terms: Public domain W3C validator