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

Theorem anassrs 629
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 588 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 421 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  anass  630  mpanr1  664  pm2.61ddan  767  pm2.61dda  768  anass1rs  782  anabss5  789  anabss7  794  pm2.61da2ne  2525  2ralbida  2582  2rexbidva  2584  pofun  4330  tfindsg2  4652  imainss  5096  eqfnfv2  5623  fnex  5741  f1elima  5787  fliftfun  5811  isores2  5830  f1oiso  5848  ovmpt2dxf  5973  grpridd  6060  sorpssuni  6286  sorpssint  6287  oalim  6531  omlim  6532  oaass  6559  omlimcl  6576  omass  6578  oelim2  6593  oeoa  6595  oeoelem  6596  nnaass  6620  omabs  6645  eroveu  6753  sbthlem4  6974  fimaxg  7104  fisupg  7105  fofinf1o  7137  ordtypelem7  7239  hartogs  7259  card2on  7268  unwdomg  7298  wemapwe  7400  dfac5  7755  cfsmolem  7896  isf32lem2  7980  ttukeylem6  8141  ondomon  8185  alephreg  8204  ltexprlem6  8665  recexsrlem  8725  wloglei  9305  recextlem2  9399  fimaxre  9701  creur  9740  uzind3OLD  10107  uz11  10250  xrmaxeq  10508  xrmineq  10509  xaddf  10551  xaddass  10569  xleadd1a  10573  xlt2add  10580  xmullem  10584  xmulgt0  10603  xmulasslem3  10606  xlemul1a  10608  xadddilem  10614  fzrevral  10866  seqcaopr2  11082  expnlbnd2  11232  faclbnd4lem4  11309  shftlem  11563  01sqrex  11735  cau3lem  11838  limsupbnd2  11957  clim2  11978  clim2c  11979  clim0c  11981  rlimresb  12039  2clim  12046  climabs0  12059  climcn1  12065  climcn2  12066  o1rlimmul  12092  climsqz  12114  climsqz2  12115  rlimsqzlem  12122  lo1le  12125  climsup  12143  caucvgrlem2  12147  iseralt  12157  summolem2  12189  fsum2dlem  12233  cvgcmp  12274  cvgcmpce  12276  climfsum  12278  fsumiun  12279  geomulcvg  12332  mertenslem2  12341  mertens  12342  smu01lem  12676  gcdcllem1  12690  gcdmultiplez  12730  dvdssq  12739  coprmdvds2  12782  pclem  12891  pcge0  12914  pcgcd1  12929  prmpwdvds  12951  1arithlem4  12973  4sqlem18  13009  vdwlem10  13037  vdwlem11  13038  ramval  13055  ramub1lem2  13074  ramcl  13076  imasaddfnlem  13430  imasaddflem  13432  imasvscafn  13439  imasleval  13443  ismon2  13637  isepi2  13644  issubc3  13723  cofucl  13762  setcmon  13919  setcepi  13920  ipodrsfi  14266  ipodrsima  14268  isacs3lem  14269  grpidpropd  14399  mhmpropd  14421  mhmima  14440  gsumccat  14464  grplcan  14534  mulgdirlem  14591  subgmulg  14635  issubg4  14638  subgint  14641  cycsubgcl  14643  ssnmz  14659  gastacl  14763  orbsta  14767  galactghm  14783  cntzsubg  14812  odmulg  14869  odbezout  14871  sylow3lem2  14939  lsmsubm  14964  efgsfo  15048  mulgmhm  15127  mulgghm  15128  gsumval3  15191  gsumcllem  15193  gsumpt  15222  gsum2d  15223  gsum2d2  15225  prdsgsum  15229  subgdmdprd  15269  dprd2d2  15279  ablfac1eu  15308  rngpropd  15372  rnglghm  15388  dvdsrpropd  15478  abvpropd  15607  islmodd  15633  lmodprop2d  15687  lsssubg  15714  lsspropd  15774  islmhm2  15795  lmhmima  15804  lsmelval2  15838  lidlsubg  15967  assapropd  16067  asclpropd  16085  psrass1lem  16123  mplcoe1  16209  mplcoe2  16211  mplind  16243  evlslem2  16249  coe1tmmul2  16352  phlpropd  16559  neips  16850  neindisj  16854  ordtrest2lem  16933  lmbrf  16990  lmss  17026  isreg2  17105  lmmo  17108  hauscmplem  17133  2ndcomap  17184  1stcelcls  17187  restlly  17209  islly2  17210  cldllycmp  17221  1stckgenlem  17248  txbas  17262  txbasval  17301  tx1cn  17303  ptpjopn  17306  ptcnp  17316  txnlly  17331  txlm  17342  xkococn  17354  fgabs  17574  fmfnfmlem4  17652  flimcf  17677  hauspwpwf1  17682  fclsbas  17716  fclscf  17720  flimfnfcls  17723  ghmcnp  17797  tgpt0  17801  tsmsxp  17837  isxmet2d  17892  elmopn2  17991  mopni3  18040  blsscls2  18050  metequiv2  18056  metss2lem  18057  met2ndci  18068  metrest  18070  metcnp  18087  metcnp2  18088  metcnpi3  18092  txmetcnp  18093  isngp4  18133  nmolb2d  18227  xrge0tsms  18339  metdsre  18357  metnrmlem3  18365  addcnlem  18368  fsumcn  18374  elcncf2  18394  mulc1cncf  18409  cncfco  18411  cncfmet  18412  bndth  18456  evth  18457  copco  18516  pcopt2  18521  pcoass  18522  pcorevlem  18524  lmmcvg  18687  lmmbrf  18688  iscau4  18705  iscauf  18706  cmetcaulem  18714  iscmet3lem3  18716  iscmet3lem1  18717  causs  18724  equivcfil  18725  lmclim  18728  caubl  18733  caublcls  18734  bcth3  18753  ivthle  18816  ivthle2  18817  ovoliunlem1  18861  ovolicc2lem5  18880  volsuplem  18912  uniioombllem6  18943  dyaddisjlem  18950  dyadmax  18953  volcn  18961  mbfmulc2lem  19002  ismbf3d  19009  mbfsup  19019  mbfinf  19020  mbflim  19023  i1fmullem  19049  itg2seq  19097  itg2uba  19098  itg2splitlem  19103  itg2split  19104  itg2monolem1  19105  ditgsplitlem  19210  ellimc2  19227  ellimc3  19229  limcflf  19231  limcmpt  19233  limcco  19243  c1lip3  19346  lhop1lem  19360  dvfsumle  19368  dvfsumabs  19370  dvfsumrlim  19378  ftc1a  19384  ftc1lem6  19388  evlsval  19403  mdegmullem  19464  elply2  19578  plypf1  19594  aalioulem2  19713  aalioulem5  19716  aalioulem6  19717  aaliou  19718  ulmcaulem  19771  ulmcau  19772  ulmss  19774  ulmdvlem3  19779  mtest  19781  itgulm  19784  abelthlem8  19815  abelth  19817  tanord  19900  cxpcn3lem  20087  mcubic  20143  cubic2  20144  dvdsflsumcom  20428  fsumdvdsmul  20435  lgsdchrval  20586  2sqlem9  20612  rplogsumlem2  20634  rpvmasumlem  20636  dchrvmasumlem1  20644  vmalogdivsum2  20687  logsqvma  20691  selberg  20697  selberg4  20710  pntibndlem3  20741  pntlem3  20758  pntleml  20760  padicabv  20779  padicabvf  20780  padicabvcxp  20781  ostth3  20787  grpolcan  20900  isgrp2d  20902  ghgrp  21035  nvmul0or  21210  sspival  21314  nmosetre  21342  blocnilem  21382  blocni  21383  h2hcau  21559  h2hlm  21560  shsel3  21894  chscllem2  22217  homulcl  22339  adjsym  22413  cnvadj  22472  hhcno  22484  hhcnf  22485  lnopl  22494  unoplin  22500  counop  22501  lnfnl  22511  hmoplin  22522  hmopm  22601  nmcexi  22606  lnconi  22613  riesz3i  22642  leopmuli  22713  leopmul  22714  hstle  22810  mdsl0  22890  mdslmd1lem2  22906  atcvatlem  22965  chirredi  22974  cdj1i  23013  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemimin  23064  isoun  23242  difioo  23275  gsumpropd2lem  23379  xrge0tsmsd  23382  conpcon  23766  cvmliftmolem2  23813  cvmliftlem6  23821  cvmliftlem8  23823  cvmlift2lem10  23843  cvmlift2lem12  23845  relexpsucl  24028  relexpcnv  24029  relexpdm  24032  relexprn  24033  relexpadd  24035  relexpindlem  24036  rtrclreclem.trans  24043  rtrclreclem.min  24044  rtrclind  24046  dedekindle  24083  dfon2lem6  24144  poseq  24253  nocvxminlem  24344  nofulllem4  24359  nofulllem5  24360  funpartfun  24481  axpasch  24569  axcontlem7  24598  axcontlem10  24601  ifscgr  24667  brsegle  24731  npincppr  25159  exopcopn  25572  comppfsc  26307  neibastop2lem  26309  cover2  26358  filbcmb  26432  fdc  26455  fdc1  26456  seqpo  26457  incsequz  26458  incsequz2  26459  metf1o  26469  lmclim2  26474  geomcau  26475  isbnd2  26507  bndss  26510  equivbnd  26514  ismtybndlem  26530  heibor1lem  26533  rrncmslem  26556  rrnequiv  26559  exidreslem  26567  ghomco  26573  isdrngo3  26590  rngoisocnv  26612  isidlc  26640  idlnegcl  26647  divrngidl  26653  intidl  26654  unichnidl  26656  keridl  26657  igenmin  26689  prnc  26692  ispridlc  26695  prter3  26750  lsmfgcl  27172  kercvrlsm  27181  frlmsslsp  27248  lindfmm  27297  islindf4  27308  hbt  27334  mamuass  27460  cntzsdrg  27510  climinf  27732  cotsqcscsq  28232  glbconxN  29567  atltcvr  29624  3dim1  29656  lvolnle3at  29771  linepsubN  29941  osumclN  30156  pexmidALTN  30167  lhpmatb  30220  cdlemg1idlemN  30761  dihlss  31440  dihglblem5aN  31482  dihatlat  31524
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator