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  2527  2ralbida  2584  2rexbidva  2586  pofun  4332  tfindsg2  4654  imainss  5098  eqfnfv2  5625  fnex  5743  f1elima  5789  fliftfun  5813  isores2  5832  f1oiso  5850  ovmpt2dxf  5975  grpridd  6062  sorpssuni  6288  sorpssint  6289  oalim  6533  omlim  6534  oaass  6561  omlimcl  6578  omass  6580  oelim2  6595  oeoa  6597  oeoelem  6598  nnaass  6622  omabs  6647  eroveu  6755  sbthlem4  6976  fimaxg  7106  fisupg  7107  fofinf1o  7139  ordtypelem7  7241  hartogs  7261  card2on  7270  unwdomg  7300  wemapwe  7402  dfac5  7757  cfsmolem  7898  isf32lem2  7982  ttukeylem6  8143  ondomon  8187  alephreg  8206  ltexprlem6  8667  recexsrlem  8727  wloglei  9307  recextlem2  9401  fimaxre  9703  creur  9742  uzind3OLD  10109  uz11  10252  xrmaxeq  10510  xrmineq  10511  xaddf  10553  xaddass  10571  xleadd1a  10575  xlt2add  10582  xmullem  10586  xmulgt0  10605  xmulasslem3  10608  xlemul1a  10610  xadddilem  10616  fzrevral  10868  seqcaopr2  11084  expnlbnd2  11234  faclbnd4lem4  11311  shftlem  11565  01sqrex  11737  cau3lem  11840  limsupbnd2  11959  clim2  11980  clim2c  11981  clim0c  11983  rlimresb  12041  2clim  12048  climabs0  12061  climcn1  12067  climcn2  12068  o1rlimmul  12094  climsqz  12116  climsqz2  12117  rlimsqzlem  12124  lo1le  12127  climsup  12145  caucvgrlem2  12149  iseralt  12159  summolem2  12191  fsum2dlem  12235  cvgcmp  12276  cvgcmpce  12278  climfsum  12280  fsumiun  12281  geomulcvg  12334  mertenslem2  12343  mertens  12344  smu01lem  12678  gcdcllem1  12692  gcdmultiplez  12732  dvdssq  12741  coprmdvds2  12784  pclem  12893  pcge0  12916  pcgcd1  12931  prmpwdvds  12953  1arithlem4  12975  4sqlem18  13011  vdwlem10  13039  vdwlem11  13040  ramval  13057  ramub1lem2  13076  ramcl  13078  imasaddfnlem  13432  imasaddflem  13434  imasvscafn  13441  imasleval  13445  ismon2  13639  isepi2  13646  issubc3  13725  cofucl  13764  setcmon  13921  setcepi  13922  ipodrsfi  14268  ipodrsima  14270  isacs3lem  14271  grpidpropd  14401  mhmpropd  14423  mhmima  14442  gsumccat  14466  grplcan  14536  mulgdirlem  14593  subgmulg  14637  issubg4  14640  subgint  14643  cycsubgcl  14645  ssnmz  14661  gastacl  14765  orbsta  14769  galactghm  14785  cntzsubg  14814  odmulg  14871  odbezout  14873  sylow3lem2  14941  lsmsubm  14966  efgsfo  15050  mulgmhm  15129  mulgghm  15130  gsumval3  15193  gsumcllem  15195  gsumpt  15224  gsum2d  15225  gsum2d2  15227  prdsgsum  15231  subgdmdprd  15271  dprd2d2  15281  ablfac1eu  15310  rngpropd  15374  rnglghm  15390  dvdsrpropd  15480  abvpropd  15609  islmodd  15635  lmodprop2d  15689  lsssubg  15716  lsspropd  15776  islmhm2  15797  lmhmima  15806  lsmelval2  15840  lidlsubg  15969  assapropd  16069  asclpropd  16087  psrass1lem  16125  mplcoe1  16211  mplcoe2  16213  mplind  16245  evlslem2  16251  coe1tmmul2  16354  phlpropd  16561  neips  16852  neindisj  16856  ordtrest2lem  16935  lmbrf  16992  lmss  17028  isreg2  17107  lmmo  17110  hauscmplem  17135  2ndcomap  17186  1stcelcls  17189  restlly  17211  islly2  17212  cldllycmp  17223  1stckgenlem  17250  txbas  17264  txbasval  17303  tx1cn  17305  ptpjopn  17308  ptcnp  17318  txnlly  17333  txlm  17344  xkococn  17356  fgabs  17576  fmfnfmlem4  17654  flimcf  17679  hauspwpwf1  17684  fclsbas  17718  fclscf  17722  flimfnfcls  17725  ghmcnp  17799  tgpt0  17803  tsmsxp  17839  isxmet2d  17894  elmopn2  17993  mopni3  18042  blsscls2  18052  metequiv2  18058  metss2lem  18059  met2ndci  18070  metrest  18072  metcnp  18089  metcnp2  18090  metcnpi3  18094  txmetcnp  18095  isngp4  18135  nmolb2d  18229  xrge0tsms  18341  metdsre  18359  metnrmlem3  18367  addcnlem  18370  fsumcn  18376  elcncf2  18396  mulc1cncf  18411  cncfco  18413  cncfmet  18414  bndth  18458  evth  18459  copco  18518  pcopt2  18523  pcoass  18524  pcorevlem  18526  lmmcvg  18689  lmmbrf  18690  iscau4  18707  iscauf  18708  cmetcaulem  18716  iscmet3lem3  18718  iscmet3lem1  18719  causs  18726  equivcfil  18727  lmclim  18730  caubl  18735  caublcls  18736  bcth3  18755  ivthle  18818  ivthle2  18819  ovoliunlem1  18863  ovolicc2lem5  18882  volsuplem  18914  uniioombllem6  18945  dyaddisjlem  18952  dyadmax  18955  volcn  18963  mbfmulc2lem  19004  ismbf3d  19011  mbfsup  19021  mbfinf  19022  mbflim  19025  i1fmullem  19051  itg2seq  19099  itg2uba  19100  itg2splitlem  19105  itg2split  19106  itg2monolem1  19107  ditgsplitlem  19212  ellimc2  19229  ellimc3  19231  limcflf  19233  limcmpt  19235  limcco  19245  c1lip3  19348  lhop1lem  19362  dvfsumle  19370  dvfsumabs  19372  dvfsumrlim  19380  ftc1a  19386  ftc1lem6  19390  evlsval  19405  mdegmullem  19466  elply2  19580  plypf1  19596  aalioulem2  19715  aalioulem5  19718  aalioulem6  19719  aaliou  19720  ulmcaulem  19773  ulmcau  19774  ulmss  19776  ulmdvlem3  19781  mtest  19783  itgulm  19786  abelthlem8  19817  abelth  19819  tanord  19902  cxpcn3lem  20089  mcubic  20145  cubic2  20146  dvdsflsumcom  20430  fsumdvdsmul  20437  lgsdchrval  20588  2sqlem9  20614  rplogsumlem2  20636  rpvmasumlem  20638  dchrvmasumlem1  20646  vmalogdivsum2  20689  logsqvma  20693  selberg  20699  selberg4  20712  pntibndlem3  20743  pntlem3  20760  pntleml  20762  padicabv  20781  padicabvf  20782  padicabvcxp  20783  ostth3  20789  grpolcan  20902  isgrp2d  20904  ghgrp  21037  nvmul0or  21212  sspival  21316  nmosetre  21344  blocnilem  21384  blocni  21385  h2hcau  21561  h2hlm  21562  shsel3  21896  chscllem2  22219  homulcl  22341  adjsym  22415  cnvadj  22474  hhcno  22486  hhcnf  22487  lnopl  22496  unoplin  22502  counop  22503  lnfnl  22513  hmoplin  22524  hmopm  22603  nmcexi  22608  lnconi  22615  riesz3i  22644  leopmuli  22715  leopmul  22716  hstle  22812  mdsl0  22892  mdslmd1lem2  22908  atcvatlem  22967  chirredi  22976  cdj1i  23015  ballotlemfc0  23053  ballotlemfcc  23054  ballotlemimin  23066  isoun  23244  difioo  23277  gsumpropd2lem  23381  xrge0tsmsd  23384  conpcon  23768  cvmliftmolem2  23815  cvmliftlem6  23823  cvmliftlem8  23825  cvmlift2lem10  23845  cvmlift2lem12  23847  relexpsucl  24030  relexpcnv  24031  relexpdm  24034  relexprn  24035  relexpadd  24037  relexpindlem  24038  rtrclreclem.trans  24045  rtrclreclem.min  24046  rtrclind  24048  dedekindle  24085  dfon2lem6  24146  poseq  24255  nocvxminlem  24346  nofulllem4  24361  nofulllem5  24362  funpartfun  24483  axpasch  24571  axcontlem7  24600  axcontlem10  24603  ifscgr  24669  brsegle  24733  npincppr  25170  exopcopn  25583  comppfsc  26318  neibastop2lem  26320  cover2  26369  filbcmb  26443  fdc  26466  fdc1  26467  seqpo  26468  incsequz  26469  incsequz2  26470  metf1o  26480  lmclim2  26485  geomcau  26486  isbnd2  26518  bndss  26521  equivbnd  26525  ismtybndlem  26541  heibor1lem  26544  rrncmslem  26567  rrnequiv  26570  exidreslem  26578  ghomco  26584  isdrngo3  26601  rngoisocnv  26623  isidlc  26651  idlnegcl  26658  divrngidl  26664  intidl  26665  unichnidl  26667  keridl  26668  igenmin  26700  prnc  26703  ispridlc  26706  prter3  26761  lsmfgcl  27183  kercvrlsm  27192  frlmsslsp  27259  lindfmm  27308  islindf4  27319  hbt  27345  mamuass  27471  cntzsdrg  27521  climinf  27743  cotsqcscsq  28243  glbconxN  29640  atltcvr  29697  3dim1  29729  lvolnle3at  29844  linepsubN  30014  osumclN  30229  pexmidALTN  30240  lhpmatb  30293  cdlemg1idlemN  30834  dihlss  31513  dihglblem5aN  31555  dihatlat  31597
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