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

Theorem anassrs 641
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 600 . 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  642  mpanr1  676  pm2.61ddan  783  pm2.61dda  784  anass1rs  798  anabss5  805  anabss7  810  pm2.61da2ne  2680  2ralbida  2744  2rexbidva  2746  pofun  4644  imainss  5240  eqfnfv2  5786  fnex  5931  f1elima  5963  fliftfun  5992  isores2  6011  f1oiso  6029  ovmpt2dxf  6205  grpridd  6292  sorpssuni  6358  sorpssint  6359  tfindsg2  6461  oalim  6960  omlim  6961  oaass  6988  omlimcl  7005  omass  7007  oelim2  7022  oeoa  7024  oeoelem  7025  nnaass  7049  omabs  7074  eroveu  7183  sbthlem4  7412  fimaxg  7547  fisupg  7548  fofinf1o  7580  ordtypelem7  7726  hartogs  7746  card2on  7757  unwdomg  7787  wemapwe  7916  wemapweOLD  7917  dfac5  8286  cfsmolem  8427  isf32lem2  8511  ttukeylem6  8671  ondomon  8715  alephreg  8734  ltexprlem6  9198  recexsrlem  9258  dedekindle  9522  wloglei  9860  recextlem2  9955  fimaxre  10265  creur  10304  uzind3OLD  10725  uz11  10871  xrmaxeq  11139  xrmineq  11140  xaddf  11182  xaddass  11200  xleadd1a  11204  xlt2add  11211  xmullem  11215  xmulgt0  11234  xmulasslem3  11237  xlemul1a  11239  xadddilem  11245  fzrevral  11528  seqcaopr2  11826  expnlbnd2  11979  faclbnd4lem4  12056  shftlem  12541  01sqrex  12723  cau3lem  12826  limsupbnd2  12945  clim2  12966  clim2c  12967  clim0c  12969  rlimresb  13027  2clim  13034  climabs0  13047  climcn1  13053  climcn2  13054  o1rlimmul  13080  climsqz  13102  climsqz2  13103  rlimsqzlem  13110  lo1le  13113  climsup  13131  caucvgrlem2  13136  iseralt  13146  summolem2  13177  fsum2dlem  13221  cvgcmp  13262  cvgcmpce  13264  climfsum  13266  fsumiun  13267  geomulcvg  13319  mertenslem2  13328  mertens  13329  smu01lem  13664  gcdcllem1  13678  gcdmultiplez  13718  dvdssq  13727  coprmdvds2  13772  pclem  13888  pcge0  13911  pcgcd1  13926  prmpwdvds  13948  1arithlem4  13970  4sqlem18  14006  vdwlem10  14034  vdwlem11  14035  ramval  14052  ramub1lem2  14071  ramcl  14073  imasaddfnlem  14449  imasaddflem  14451  imasvscafn  14458  imasleval  14462  ismon2  14656  isepi2  14663  issubc3  14742  cofucl  14781  setcmon  14938  setcepi  14939  ipodrsfi  15316  ipodrsima  15318  isacs3lem  15319  grpidpropd  15430  mhmpropd  15453  mhmima  15473  gsumccat  15499  grplcan  15570  mulgdirlem  15631  subgmulg  15675  issubg4  15680  subgint  15685  cycsubgcl  15687  ssnmz  15703  gastacl  15807  orbsta  15811  cntzsubg  15834  galactghm  15888  odmulg  16037  odbezout  16039  sylow3lem2  16107  lsmsubm  16132  efgsfo  16216  mulgmhm  16295  mulgghm  16296  gsumval3OLD  16362  gsumval3  16365  gsumcllem  16366  gsumcllemOLD  16367  gsumpt  16429  gsumptOLD  16430  gsum2d  16437  gsum2dOLD  16438  gsum2d2  16440  prdsgsum  16445  prdsgsumOLD  16446  subgdmdprd  16505  dprd2d2  16517  ablfac1eu  16548  rngpropd  16612  rnglghm  16628  dvdsrpropd  16722  abvpropd  16851  islmodd  16878  lmodprop2d  16931  lsssubg  16960  lsspropd  17020  islmhm2  17041  lmhmima  17050  lsmelval2  17088  lidlsubg  17219  assapropd  17320  asclpropd  17338  psrass1lem  17381  mplcoe1  17478  mplcoe2  17481  mplcoe2OLD  17482  mplind  17516  evlslem2  17525  coe1tmmul2  17627  phlpropd  17926  frlmsslsp  18065  frlmsslspOLD  18066  lindfmm  18098  islindf4  18109  mamuass  18148  mavmulass  18202  mdetuni0  18269  mdetmul  18271  neips  18559  neindisj  18563  ordtrest2lem  18649  lmbrf  18706  lmss  18744  isreg2  18823  lmmo  18826  hauscmplem  18851  bwth  18855  2ndcomap  18904  1stcelcls  18907  restlly  18929  islly2  18930  cldllycmp  18941  1stckgenlem  18968  txbas  18982  txbasval  19021  tx1cn  19024  ptpjopn  19027  ptcnp  19037  txnlly  19052  txlm  19063  xkococn  19075  fgabs  19294  fmfnfmlem4  19372  flimcf  19397  hauspwpwf1  19402  fclsbas  19436  fclscf  19440  flimfnfcls  19443  ghmcnp  19527  tgpt0  19531  tsmsxp  19571  isxmet2d  19744  elmopn2  19862  mopni3  19911  blsscls2  19921  metequiv2  19927  metss2lem  19928  met2ndci  19939  metrest  19941  metcnp  19958  metcnp2  19959  metcnpi3  19963  txmetcnp  19964  isngp4  20045  nmolb2d  20139  xrge0tsms  20253  metdsre  20271  metnrmlem3  20279  addcnlem  20282  fsumcn  20288  elcncf2  20308  mulc1cncf  20323  cncfco  20325  cncfmet  20326  bndth  20372  evth  20373  copco  20432  pcopt2  20437  pcoass  20438  pcorevlem  20440  lmmcvg  20614  lmmbrf  20615  iscau4  20632  iscauf  20633  cmetcaulem  20641  iscmet3lem3  20643  iscmet3lem1  20644  causs  20651  equivcfil  20652  lmclim  20655  caubl  20660  caublcls  20661  bcth3  20684  ivthle  20782  ivthle2  20783  ovoliunlem1  20827  ovolicc2lem5  20846  volsuplem  20878  uniioombllem6  20910  dyaddisjlem  20917  dyadmax  20920  volcn  20928  mbfmulc2lem  20967  ismbf3d  20974  mbfsup  20984  mbfinf  20985  mbflim  20988  i1fmullem  21014  itg2seq  21062  itg2uba  21063  itg2splitlem  21068  itg2split  21069  itg2monolem1  21070  ditgsplitlem  21177  ellimc2  21194  ellimc3  21196  limcflf  21198  limcmpt  21200  limcco  21210  c1lip3  21313  lhop1lem  21327  dvfsumle  21335  dvfsumabs  21337  dvfsumrlim  21345  ftc1a  21351  ftc1lem6  21355  evlsval  21371  mdegmullem  21434  elply2  21549  plypf1  21565  aalioulem2  21684  aalioulem5  21687  aalioulem6  21688  aaliou  21689  ulmcaulem  21744  ulmcau  21745  ulmss  21747  ulmdvlem3  21752  mtest  21754  itgulm  21758  abelthlem8  21789  abelth  21791  tanord  21879  cxpcn3lem  22070  mcubic  22127  cubic2  22128  dvdsflsumcom  22413  fsumdvdsmul  22420  lgsdchrval  22571  2sqlem9  22597  rplogsumlem2  22619  rpvmasumlem  22621  dchrvmasumlem1  22629  vmalogdivsum2  22672  logsqvma  22676  selberg  22682  selberg4  22695  pntibndlem3  22726  pntlem3  22743  pntleml  22745  padicabv  22764  padicabvf  22765  padicabvcxp  22766  ostth3  22772  axpasch  23010  axcontlem7  23039  axcontlem10  23042  cusgrasize2inds  23208  grpolcan  23543  isgrp2d  23545  ghgrp  23678  nvmul0or  23855  sspival  23959  nmosetre  23987  blocnilem  24027  blocni  24028  h2hcau  24204  h2hlm  24205  shsel3  24541  chscllem2  24864  homulcl  24986  adjsym  25060  cnvadj  25119  hhcno  25131  hhcnf  25132  lnopl  25141  unoplin  25147  counop  25148  lnfnl  25158  hmoplin  25169  hmopm  25248  nmcexi  25253  lnconi  25260  riesz3i  25289  leopmuli  25360  leopmul  25361  hstle  25457  mdsl0  25537  mdslmd1lem2  25553  atcvatlem  25612  chirredi  25621  cdj1i  25660  isoun  25821  difioo  25895  gsumpropd2lem  26093  xrge0tsmsd  26106  pstmxmet  26178  ordtrest2NEWlem  26206  dya2icoseg2  26547  eulerpartlemgc  26593  eulerpartlemgvv  26607  eulerpartlemgh  26609  eulerpartlemgs2  26611  ballotlemimin  26736  signstfvneq0  26821  conpcon  26972  cvmliftmolem2  27019  cvmliftlem6  27027  cvmliftlem8  27029  cvmlift2lem10  27049  cvmlift2lem12  27051  relexpsucl  27181  relexpcnv  27182  relexpdm  27184  relexprn  27185  relexpadd  27187  relexpindlem  27188  rtrclreclem.trans  27195  rtrclreclem.min  27196  rtrclind  27198  prodfn0  27256  prodfrec  27257  zprod  27297  fprodeq0  27333  fprodn0  27337  fprod2dlem  27338  dfon2lem6  27448  poseq  27561  nocvxminlem  27678  nofulllem4  27693  nofulllem5  27694  ifscgr  27922  brsegle  27986  finixpnum  28258  fin2solem  28259  fin2so  28260  heicant  28270  itg2gt0cn  28291  bddiblnc  28306  ftc1cnnc  28310  ftc1anclem5  28315  ftc1anclem6  28316  ftc1anclem7  28317  ftc1anc  28319  comppfsc  28423  neibastop2lem  28425  cover2  28451  filbcmb  28478  fdc  28485  fdc1  28486  seqpo  28487  incsequz  28488  incsequz2  28489  metf1o  28495  lmclim2  28498  geomcau  28499  isbnd2  28526  bndss  28529  equivbnd  28533  ismtybndlem  28549  heibor1lem  28552  rrncmslem  28575  rrnequiv  28578  exidreslem  28586  ghomco  28592  isdrngo3  28609  rngoisocnv  28631  isidlc  28659  idlnegcl  28666  divrngidl  28672  intidl  28673  unichnidl  28675  keridl  28676  igenmin  28708  prnc  28711  ispridlc  28714  prter3  28872  lsmfgcl  29272  kercvrlsm  29281  unxpwdom3  29293  hbt  29331  cntzsdrg  29404  climinf  29625  2spotdisj  30500  ovmpt2rdxf  30573  cotsqcscsq  30806  glbconxN  32595  atltcvr  32652  3dim1  32684  lvolnle3at  32799  linepsubN  32969  osumclN  33184  pexmidALTN  33195  lhpmatb  33248  cdlemg1idlemN  33789  dihlss  34468  dihglblem5aN  34510  dihatlat  34552
  Copyright terms: Public domain W3C validator