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

Theorem anassrs 631
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 590 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 423 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  anass  632  mpanr1  666  pm2.61ddan  769  pm2.61dda  770  anass1rs  784  anabss5  791  anabss7  796  pm2.61da2ne  2689  2ralbida  2750  2rexbidva  2752  pofun  4548  tfindsg2  4870  imainss  5316  eqfnfv2  5857  fnex  5990  f1elima  6038  fliftfun  6063  isores2  6082  f1oiso  6100  ovmpt2dxf  6228  grpridd  6316  sorpssuni  6560  sorpssint  6561  oalim  6805  omlim  6806  oaass  6833  omlimcl  6850  omass  6852  oelim2  6867  oeoa  6869  oeoelem  6870  nnaass  6894  omabs  6919  eroveu  7028  sbthlem4  7249  fimaxg  7383  fisupg  7384  fofinf1o  7416  ordtypelem7  7522  hartogs  7542  card2on  7551  unwdomg  7581  wemapwe  7683  dfac5  8040  cfsmolem  8181  isf32lem2  8265  ttukeylem6  8425  ondomon  8469  alephreg  8488  ltexprlem6  8949  recexsrlem  9009  wloglei  9590  recextlem2  9684  fimaxre  9986  creur  10025  uzind3OLD  10396  uz11  10539  xrmaxeq  10798  xrmineq  10799  xaddf  10841  xaddass  10859  xleadd1a  10863  xlt2add  10870  xmullem  10874  xmulgt0  10893  xmulasslem3  10896  xlemul1a  10898  xadddilem  10904  fzrevral  11162  seqcaopr2  11390  expnlbnd2  11541  faclbnd4lem4  11618  shftlem  11914  01sqrex  12086  cau3lem  12189  limsupbnd2  12308  clim2  12329  clim2c  12330  clim0c  12332  rlimresb  12390  2clim  12397  climabs0  12410  climcn1  12416  climcn2  12417  o1rlimmul  12443  climsqz  12465  climsqz2  12466  rlimsqzlem  12473  lo1le  12476  climsup  12494  caucvgrlem2  12499  iseralt  12509  summolem2  12541  fsum2dlem  12585  cvgcmp  12626  cvgcmpce  12628  climfsum  12630  fsumiun  12631  geomulcvg  12684  mertenslem2  12693  mertens  12694  smu01lem  13028  gcdcllem1  13042  gcdmultiplez  13082  dvdssq  13091  coprmdvds2  13134  pclem  13243  pcge0  13266  pcgcd1  13281  prmpwdvds  13303  1arithlem4  13325  4sqlem18  13361  vdwlem10  13389  vdwlem11  13390  ramval  13407  ramub1lem2  13426  ramcl  13428  imasaddfnlem  13784  imasaddflem  13786  imasvscafn  13793  imasleval  13797  ismon2  13991  isepi2  13998  issubc3  14077  cofucl  14116  setcmon  14273  setcepi  14274  ipodrsfi  14620  ipodrsima  14622  isacs3lem  14623  grpidpropd  14753  mhmpropd  14775  mhmima  14794  gsumccat  14818  grplcan  14888  mulgdirlem  14945  subgmulg  14989  issubg4  14992  subgint  14995  cycsubgcl  14997  ssnmz  15013  gastacl  15117  orbsta  15121  galactghm  15137  cntzsubg  15166  odmulg  15223  odbezout  15225  sylow3lem2  15293  lsmsubm  15318  efgsfo  15402  mulgmhm  15481  mulgghm  15482  gsumval3  15545  gsumcllem  15547  gsumpt  15576  gsum2d  15577  gsum2d2  15579  prdsgsum  15583  subgdmdprd  15623  dprd2d2  15633  ablfac1eu  15662  rngpropd  15726  rnglghm  15742  dvdsrpropd  15832  abvpropd  15961  islmodd  15987  lmodprop2d  16037  lsssubg  16064  lsspropd  16124  islmhm2  16145  lmhmima  16154  lsmelval2  16188  lidlsubg  16317  assapropd  16417  asclpropd  16435  psrass1lem  16473  mplcoe1  16559  mplcoe2  16561  mplind  16593  evlslem2  16599  coe1tmmul2  16699  phlpropd  16917  neips  17208  neindisj  17212  ordtrest2lem  17298  lmbrf  17355  lmss  17393  isreg2  17472  lmmo  17475  hauscmplem  17500  2ndcomap  17552  1stcelcls  17555  restlly  17577  islly2  17578  cldllycmp  17589  1stckgenlem  17616  txbas  17630  txbasval  17669  tx1cn  17672  ptpjopn  17675  ptcnp  17685  txnlly  17700  txlm  17711  xkococn  17723  fgabs  17942  fmfnfmlem4  18020  flimcf  18045  hauspwpwf1  18050  fclsbas  18084  fclscf  18088  flimfnfcls  18091  ghmcnp  18175  tgpt0  18179  tsmsxp  18215  isxmet2d  18388  elmopn2  18506  mopni3  18555  blsscls2  18565  metequiv2  18571  metss2lem  18572  met2ndci  18583  metrest  18585  metcnp  18602  metcnp2  18603  metcnpi3  18607  txmetcnp  18608  isngp4  18689  nmolb2d  18783  xrge0tsms  18896  metdsre  18914  metnrmlem3  18922  addcnlem  18925  fsumcn  18931  elcncf2  18951  mulc1cncf  18966  cncfco  18968  cncfmet  18969  bndth  19014  evth  19015  copco  19074  pcopt2  19079  pcoass  19080  pcorevlem  19082  lmmcvg  19245  lmmbrf  19246  iscau4  19263  iscauf  19264  cmetcaulem  19272  iscmet3lem3  19274  iscmet3lem1  19275  causs  19282  equivcfil  19283  lmclim  19286  caubl  19291  caublcls  19292  bcth3  19315  ivthle  19384  ivthle2  19385  ovoliunlem1  19429  ovolicc2lem5  19448  volsuplem  19480  uniioombllem6  19511  dyaddisjlem  19518  dyadmax  19521  volcn  19529  mbfmulc2lem  19568  ismbf3d  19575  mbfsup  19585  mbfinf  19586  mbflim  19589  i1fmullem  19615  itg2seq  19663  itg2uba  19664  itg2splitlem  19669  itg2split  19670  itg2monolem1  19671  ditgsplitlem  19778  ellimc2  19795  ellimc3  19797  limcflf  19799  limcmpt  19801  limcco  19811  c1lip3  19914  lhop1lem  19928  dvfsumle  19936  dvfsumabs  19938  dvfsumrlim  19946  ftc1a  19952  ftc1lem6  19956  evlsval  19971  mdegmullem  20032  elply2  20146  plypf1  20162  aalioulem2  20281  aalioulem5  20284  aalioulem6  20285  aaliou  20286  ulmcaulem  20341  ulmcau  20342  ulmss  20344  ulmdvlem3  20349  mtest  20351  itgulm  20355  abelthlem8  20386  abelth  20388  tanord  20471  cxpcn3lem  20662  mcubic  20718  cubic2  20719  dvdsflsumcom  21004  fsumdvdsmul  21011  lgsdchrval  21162  2sqlem9  21188  rplogsumlem2  21210  rpvmasumlem  21212  dchrvmasumlem1  21220  vmalogdivsum2  21263  logsqvma  21267  selberg  21273  selberg4  21286  pntibndlem3  21317  pntlem3  21334  pntleml  21336  padicabv  21355  padicabvf  21356  padicabvcxp  21357  ostth3  21363  cusgrasize2inds  21517  grpolcan  21852  isgrp2d  21854  ghgrp  21987  nvmul0or  22164  sspival  22268  nmosetre  22296  blocnilem  22336  blocni  22337  h2hcau  22513  h2hlm  22514  shsel3  22848  chscllem2  23171  homulcl  23293  adjsym  23367  cnvadj  23426  hhcno  23438  hhcnf  23439  lnopl  23448  unoplin  23454  counop  23455  lnfnl  23465  hmoplin  23476  hmopm  23555  nmcexi  23560  lnconi  23567  riesz3i  23596  leopmuli  23667  leopmul  23668  hstle  23764  mdsl0  23844  mdslmd1lem2  23860  atcvatlem  23919  chirredi  23928  cdj1i  23967  isoun  24120  difioo  24176  gsumpropd2lem  24251  xrge0tsmsd  24254  pstmxmet  24323  dya2icoseg2  24659  ballotlemimin  24794  conpcon  24953  cvmliftmolem2  25000  cvmliftlem6  25008  cvmliftlem8  25010  cvmlift2lem10  25030  cvmlift2lem12  25032  relexpsucl  25163  relexpcnv  25164  relexpdm  25166  relexprn  25167  relexpadd  25169  relexpindlem  25170  rtrclreclem.trans  25177  rtrclreclem.min  25178  rtrclind  25180  dedekindle  25219  prodfn0  25253  prodfrec  25254  zprod  25294  fprodeq0  25330  fprodn0  25334  fprod2dlem  25335  dfon2lem6  25446  poseq  25559  nocvxminlem  25676  nofulllem4  25691  nofulllem5  25692  axpasch  25911  axcontlem7  25940  axcontlem10  25943  ifscgr  26009  brsegle  26073  heicant  26277  itg2gt0cn  26298  bddiblnc  26313  ftc1cnnc  26317  ftc1anclem5  26322  ftc1anclem6  26323  ftc1anclem7  26324  ftc1anc  26326  comppfsc  26425  neibastop2lem  26427  cover2  26453  filbcmb  26480  fdc  26487  fdc1  26488  seqpo  26489  incsequz  26490  incsequz2  26491  metf1o  26499  lmclim2  26502  geomcau  26503  isbnd2  26530  bndss  26533  equivbnd  26537  ismtybndlem  26553  heibor1lem  26556  rrncmslem  26579  rrnequiv  26582  exidreslem  26590  ghomco  26596  isdrngo3  26613  rngoisocnv  26635  isidlc  26663  idlnegcl  26670  divrngidl  26676  intidl  26677  unichnidl  26679  keridl  26680  igenmin  26712  prnc  26715  ispridlc  26718  prter3  26769  lsmfgcl  27187  kercvrlsm  27196  frlmsslsp  27263  lindfmm  27312  islindf4  27323  hbt  27349  mamuass  27475  cntzsdrg  27525  climinf  27746  2spotdisj  28548  cotsqcscsq  28603  glbconxN  30273  atltcvr  30330  3dim1  30362  lvolnle3at  30477  linepsubN  30647  osumclN  30862  pexmidALTN  30873  lhpmatb  30926  cdlemg1idlemN  31467  dihlss  32146  dihglblem5aN  32188  dihatlat  32230
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 179  df-an 362
  Copyright terms: Public domain W3C validator