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  790  pm2.61dda  791  anass1rs  805  anabss5  814  anabss7  819  pm2.61da2ne  2786  ralimdvva  2875  2ralbida  2905  2ralbidva  2906  2rexbidva  2979  copsexg  4732  pofun  4816  imainss  5419  eqfnfv2  5974  fnex  6125  f1elima  6157  fliftfun  6196  isores2  6215  f1oiso  6233  ovmpt2dxf  6410  grpridd  6497  sorpssuni  6571  sorpssint  6572  tfindsg2  6674  oalim  7179  omlim  7180  oaass  7207  omlimcl  7224  omass  7226  oelim2  7241  oeoa  7243  oeoelem  7244  nnaass  7268  omabs  7293  eroveu  7403  sbthlem4  7627  fimaxg  7763  fisupg  7764  fofinf1o  7797  ordtypelem7  7945  hartogs  7965  card2on  7976  unwdomg  8006  wemapwe  8135  wemapweOLD  8136  dfac5  8505  cfsmolem  8646  isf32lem2  8730  ttukeylem6  8890  ondomon  8934  alephreg  8953  ltexprlem6  9415  recexsrlem  9476  dedekindle  9740  wloglei  10081  recextlem2  10176  fimaxre  10486  creur  10526  uzind3OLD  10952  uz11  11100  xrmaxeq  11376  xrmineq  11377  xaddf  11419  xaddass  11437  xleadd1a  11441  xlt2add  11448  xmullem  11452  xmulgt0  11471  xmulasslem3  11474  xlemul1a  11476  xadddilem  11482  fzrevral  11758  seqcaopr2  12106  expnlbnd2  12259  faclbnd4lem4  12336  shftlem  12858  01sqrex  13040  cau3lem  13143  limsupbnd2  13262  clim2  13283  clim2c  13284  clim0c  13286  rlimresb  13344  2clim  13351  climabs0  13364  climcn1  13370  climcn2  13371  o1rlimmul  13397  climsqz  13419  climsqz2  13420  rlimsqzlem  13427  lo1le  13430  climsup  13448  caucvgrlem2  13453  iseralt  13463  summolem2  13494  fsum2dlem  13541  cvgcmp  13586  cvgcmpce  13588  climfsum  13590  fsumiun  13591  geomulcvg  13641  mertenslem2  13650  mertens  13651  smu01lem  13987  gcdcllem1  14001  gcdmultiplez  14041  dvdssq  14050  coprmdvds2  14096  pclem  14214  pcge0  14237  pcgcd1  14252  prmpwdvds  14274  1arithlem4  14296  4sqlem18  14332  vdwlem10  14360  vdwlem11  14361  ramval  14378  ramub1lem2  14397  ramcl  14399  imasaddfnlem  14776  imasaddflem  14778  imasvscafn  14785  imasleval  14789  ismon2  14983  isepi2  14990  issubc3  15069  cofucl  15108  setcmon  15265  setcepi  15266  ipodrsfi  15643  ipodrsima  15645  isacs3lem  15646  grpidpropd  15757  mhmpropd  15780  mhmima  15801  gsumpropd2lem  15815  gsumccat  15829  grplcan  15900  mulgdirlem  15963  subgmulg  16007  issubg4  16012  subgint  16017  cycsubgcl  16019  ssnmz  16035  gastacl  16139  orbsta  16143  cntzsubg  16166  galactghm  16220  odmulg  16371  odbezout  16373  sylow3lem2  16441  lsmsubm  16466  efgsfo  16550  mulgmhm  16629  mulgghm  16630  gsumval3OLD  16696  gsumval3  16699  gsumcllem  16700  gsumcllemOLD  16701  gsumpt  16776  gsumptOLD  16777  gsum2d  16787  gsum2dOLD  16788  gsum2d2  16790  prdsgsum  16795  prdsgsumOLD  16796  subgdmdprd  16868  dprd2d2  16880  ablfac1eu  16911  srglmhm  16971  srgrmhm  16972  rngpropd  17014  rnglghm  17031  dvdsrpropd  17126  abvpropd  17271  islmodd  17298  lmodprop2d  17352  lsssubg  17383  lsspropd  17443  islmhm2  17464  lmhmima  17473  lsmelval2  17511  lidlsubg  17642  assapropd  17744  asclpropd  17763  psrass1lem  17797  mplcoe1  17895  mplcoe5  17899  mplcoe2OLD  17901  mplind  17935  evlslem2  17948  evlsval  17956  coe1tmmul2  18085  phlpropd  18454  frlmsslsp  18593  frlmsslspOLD  18594  lindfmm  18626  islindf4  18637  mamuass  18668  mavmulass  18815  mdetuni0  18887  mdetmul  18889  cpmatacl  18981  cpmadugsumfi  19142  cpmadugsum  19143  cpmadumatpolylem1  19146  cpmadumatpolylem2  19147  cpmadumatpoly  19148  cayhamlem4  19153  neips  19377  neindisj  19381  ordtrest2lem  19467  lmbrf  19524  lmss  19562  isreg2  19641  lmmo  19644  hauscmplem  19669  bwth  19673  2ndcomap  19722  1stcelcls  19725  restlly  19747  islly2  19748  cldllycmp  19759  1stckgenlem  19786  txbas  19800  txbasval  19839  tx1cn  19842  ptpjopn  19845  ptcnp  19855  txnlly  19870  txlm  19881  xkococn  19893  fgabs  20112  fmfnfmlem4  20190  flimcf  20215  hauspwpwf1  20220  fclsbas  20254  fclscf  20258  flimfnfcls  20261  ghmcnp  20345  tgpt0  20349  tsmsxp  20389  isxmet2d  20562  elmopn2  20680  mopni3  20729  blsscls2  20739  metequiv2  20745  metss2lem  20746  met2ndci  20757  metrest  20759  metcnp  20776  metcnp2  20777  metcnpi3  20781  txmetcnp  20782  isngp4  20863  nmolb2d  20957  xrge0tsms  21071  metdsre  21089  metnrmlem3  21097  addcnlem  21100  fsumcn  21106  elcncf2  21126  mulc1cncf  21141  cncfco  21143  cncfmet  21144  bndth  21190  evth  21191  copco  21250  pcopt2  21255  pcoass  21256  pcorevlem  21258  lmmcvg  21432  lmmbrf  21433  iscau4  21450  iscauf  21451  cmetcaulem  21459  iscmet3lem3  21461  iscmet3lem1  21462  causs  21469  equivcfil  21470  lmclim  21473  caubl  21478  caublcls  21479  bcth3  21502  ivthle  21600  ivthle2  21601  ovoliunlem1  21645  ovolicc2lem5  21664  volsuplem  21697  uniioombllem6  21729  dyaddisjlem  21736  dyadmax  21739  volcn  21747  mbfmulc2lem  21786  ismbf3d  21793  mbfsup  21803  mbfinf  21804  mbflim  21807  i1fmullem  21833  itg2seq  21881  itg2uba  21882  itg2splitlem  21887  itg2split  21888  itg2monolem1  21889  ditgsplitlem  21996  ellimc2  22013  ellimc3  22015  limcflf  22017  limcmpt  22019  limcco  22029  c1lip3  22132  lhop1lem  22146  dvfsumle  22154  dvfsumabs  22156  dvfsumrlim  22164  ftc1a  22170  ftc1lem6  22174  mdegmullem  22210  elply2  22325  plypf1  22341  aalioulem2  22460  aalioulem5  22463  aalioulem6  22464  aaliou  22465  ulmcaulem  22520  ulmcau  22521  ulmss  22523  ulmdvlem3  22528  mtest  22530  itgulm  22534  abelthlem8  22565  abelth  22567  tanord  22655  cxpcn3lem  22846  mcubic  22903  cubic2  22904  dvdsflsumcom  23189  fsumdvdsmul  23196  lgsdchrval  23347  2sqlem9  23373  rplogsumlem2  23395  rpvmasumlem  23397  dchrvmasumlem1  23405  vmalogdivsum2  23448  logsqvma  23452  selberg  23458  selberg4  23471  pntibndlem3  23502  pntlem3  23519  pntleml  23521  padicabv  23540  padicabvf  23541  padicabvcxp  23542  ostth3  23548  axpasch  23917  axcontlem7  23946  axcontlem10  23949  cusgrasize2inds  24150  2spotdisj  24735  grpolcan  24908  isgrp2d  24910  ghgrp  25043  nvmul0or  25220  sspival  25324  nmosetre  25352  blocnilem  25392  blocni  25393  h2hcau  25569  h2hlm  25570  shsel3  25906  chscllem2  26229  homulcl  26351  adjsym  26425  cnvadj  26484  hhcno  26496  hhcnf  26497  lnopl  26506  unoplin  26512  counop  26513  lnfnl  26523  hmoplin  26534  hmopm  26613  nmcexi  26618  lnconi  26625  riesz3i  26654  leopmuli  26725  leopmul  26726  hstle  26822  mdsl0  26902  mdslmd1lem2  26918  atcvatlem  26977  chirredi  26986  cdj1i  27025  isoun  27189  difioo  27258  xrge0tsmsd  27435  pstmxmet  27509  ordtrest2NEWlem  27537  dya2icoseg2  27886  eulerpartlemgc  27938  eulerpartlemgvv  27952  eulerpartlemgh  27954  eulerpartlemgs2  27956  ballotlemimin  28081  signstfvneq0  28166  conpcon  28317  cvmliftmolem2  28364  cvmliftlem6  28372  cvmliftlem8  28374  cvmlift2lem10  28394  cvmlift2lem12  28396  relexpsucl  28527  relexpcnv  28528  relexpdm  28530  relexprn  28531  relexpadd  28533  relexpindlem  28534  rtrclreclem.trans  28541  rtrclreclem.min  28542  rtrclind  28544  prodfn0  28602  prodfrec  28603  zprod  28643  fprodeq0  28679  fprodn0  28683  fprod2dlem  28684  dfon2lem6  28794  poseq  28907  nocvxminlem  29024  nofulllem4  29039  nofulllem5  29040  ifscgr  29268  brsegle  29332  finixpnum  29612  fin2solem  29613  fin2so  29614  heicant  29624  itg2gt0cn  29645  bddiblnc  29660  ftc1cnnc  29664  ftc1anclem5  29669  ftc1anclem6  29670  ftc1anclem7  29671  ftc1anc  29673  comppfsc  29777  neibastop2lem  29779  cover2  29805  filbcmb  29832  fdc  29839  fdc1  29840  seqpo  29841  incsequz  29842  incsequz2  29843  metf1o  29849  lmclim2  29852  geomcau  29853  isbnd2  29880  bndss  29883  equivbnd  29887  ismtybndlem  29903  heibor1lem  29906  rrncmslem  29929  rrnequiv  29932  exidreslem  29940  ghomco  29946  isdrngo3  29963  rngoisocnv  29985  isidlc  30013  idlnegcl  30020  divrngidl  30026  intidl  30027  unichnidl  30029  keridl  30030  igenmin  30062  prnc  30065  ispridlc  30068  prter3  30225  lsmfgcl  30624  kercvrlsm  30633  unxpwdom3  30645  hbt  30683  cntzsdrg  30756  lcmgcdlem  30812  lcmdvds  30814  climinf  31148  clim2f  31178  clim2cf  31192  clim0cf  31196  fourierdlem83  31490  ovmpt2rdxf  31992  cotsqcscsq  32237  glbconxN  34174  atltcvr  34231  3dim1  34263  lvolnle3at  34378  linepsubN  34548  osumclN  34763  pexmidALTN  34774  lhpmatb  34827  cdlemg1idlemN  35368  dihlss  36047  dihglblem5aN  36089  dihatlat  36131
  Copyright terms: Public domain W3C validator