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

Theorem anassrs 630
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 589 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 422 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  anass  631  mpanr1  665  pm2.61ddan  768  pm2.61dda  769  anass1rs  783  anabss5  790  anabss7  795  pm2.61da2ne  2622  2ralbida  2681  2rexbidva  2683  pofun  4453  tfindsg2  4774  imainss  5220  eqfnfv2  5760  fnex  5893  f1elima  5941  fliftfun  5966  isores2  5985  f1oiso  6003  ovmpt2dxf  6131  grpridd  6219  sorpssuni  6460  sorpssint  6461  oalim  6705  omlim  6706  oaass  6733  omlimcl  6750  omass  6752  oelim2  6767  oeoa  6769  oeoelem  6770  nnaass  6794  omabs  6819  eroveu  6928  sbthlem4  7149  fimaxg  7283  fisupg  7284  fofinf1o  7316  ordtypelem7  7419  hartogs  7439  card2on  7448  unwdomg  7478  wemapwe  7580  dfac5  7935  cfsmolem  8076  isf32lem2  8160  ttukeylem6  8320  ondomon  8364  alephreg  8383  ltexprlem6  8844  recexsrlem  8904  wloglei  9484  recextlem2  9578  fimaxre  9880  creur  9919  uzind3OLD  10290  uz11  10433  xrmaxeq  10692  xrmineq  10693  xaddf  10735  xaddass  10753  xleadd1a  10757  xlt2add  10764  xmullem  10768  xmulgt0  10787  xmulasslem3  10790  xlemul1a  10792  xadddilem  10798  fzrevral  11054  seqcaopr2  11279  expnlbnd2  11430  faclbnd4lem4  11507  shftlem  11803  01sqrex  11975  cau3lem  12078  limsupbnd2  12197  clim2  12218  clim2c  12219  clim0c  12221  rlimresb  12279  2clim  12286  climabs0  12299  climcn1  12305  climcn2  12306  o1rlimmul  12332  climsqz  12354  climsqz2  12355  rlimsqzlem  12362  lo1le  12365  climsup  12383  caucvgrlem2  12388  iseralt  12398  summolem2  12430  fsum2dlem  12474  cvgcmp  12515  cvgcmpce  12517  climfsum  12519  fsumiun  12520  geomulcvg  12573  mertenslem2  12582  mertens  12583  smu01lem  12917  gcdcllem1  12931  gcdmultiplez  12971  dvdssq  12980  coprmdvds2  13023  pclem  13132  pcge0  13155  pcgcd1  13170  prmpwdvds  13192  1arithlem4  13214  4sqlem18  13250  vdwlem10  13278  vdwlem11  13279  ramval  13296  ramub1lem2  13315  ramcl  13317  imasaddfnlem  13673  imasaddflem  13675  imasvscafn  13682  imasleval  13686  ismon2  13880  isepi2  13887  issubc3  13966  cofucl  14005  setcmon  14162  setcepi  14163  ipodrsfi  14509  ipodrsima  14511  isacs3lem  14512  grpidpropd  14642  mhmpropd  14664  mhmima  14683  gsumccat  14707  grplcan  14777  mulgdirlem  14834  subgmulg  14878  issubg4  14881  subgint  14884  cycsubgcl  14886  ssnmz  14902  gastacl  15006  orbsta  15010  galactghm  15026  cntzsubg  15055  odmulg  15112  odbezout  15114  sylow3lem2  15182  lsmsubm  15207  efgsfo  15291  mulgmhm  15370  mulgghm  15371  gsumval3  15434  gsumcllem  15436  gsumpt  15465  gsum2d  15466  gsum2d2  15468  prdsgsum  15472  subgdmdprd  15512  dprd2d2  15522  ablfac1eu  15551  rngpropd  15615  rnglghm  15631  dvdsrpropd  15721  abvpropd  15850  islmodd  15876  lmodprop2d  15926  lsssubg  15953  lsspropd  16013  islmhm2  16034  lmhmima  16043  lsmelval2  16077  lidlsubg  16206  assapropd  16306  asclpropd  16324  psrass1lem  16362  mplcoe1  16448  mplcoe2  16450  mplind  16482  evlslem2  16488  coe1tmmul2  16588  phlpropd  16802  neips  17093  neindisj  17097  ordtrest2lem  17182  lmbrf  17239  lmss  17277  isreg2  17356  lmmo  17359  hauscmplem  17384  2ndcomap  17435  1stcelcls  17438  restlly  17460  islly2  17461  cldllycmp  17472  1stckgenlem  17499  txbas  17513  txbasval  17552  tx1cn  17555  ptpjopn  17558  ptcnp  17568  txnlly  17583  txlm  17594  xkococn  17606  fgabs  17825  fmfnfmlem4  17903  flimcf  17928  hauspwpwf1  17933  fclsbas  17967  fclscf  17971  flimfnfcls  17974  ghmcnp  18058  tgpt0  18062  tsmsxp  18098  isxmet2d  18259  elmopn2  18358  mopni3  18407  blsscls2  18417  metequiv2  18423  metss2lem  18424  met2ndci  18435  metrest  18437  metcnp  18454  metcnp2  18455  metcnpi3  18459  txmetcnp  18460  isngp4  18522  nmolb2d  18616  xrge0tsms  18729  metdsre  18747  metnrmlem3  18755  addcnlem  18758  fsumcn  18764  elcncf2  18784  mulc1cncf  18799  cncfco  18801  cncfmet  18802  bndth  18847  evth  18848  copco  18907  pcopt2  18912  pcoass  18913  pcorevlem  18915  lmmcvg  19078  lmmbrf  19079  iscau4  19096  iscauf  19097  cmetcaulem  19105  iscmet3lem3  19107  iscmet3lem1  19108  causs  19115  equivcfil  19116  lmclim  19119  caubl  19124  caublcls  19125  bcth3  19146  ivthle  19213  ivthle2  19214  ovoliunlem1  19258  ovolicc2lem5  19277  volsuplem  19309  uniioombllem6  19340  dyaddisjlem  19347  dyadmax  19350  volcn  19358  mbfmulc2lem  19399  ismbf3d  19406  mbfsup  19416  mbfinf  19417  mbflim  19420  i1fmullem  19446  itg2seq  19494  itg2uba  19495  itg2splitlem  19500  itg2split  19501  itg2monolem1  19502  ditgsplitlem  19607  ellimc2  19624  ellimc3  19626  limcflf  19628  limcmpt  19630  limcco  19640  c1lip3  19743  lhop1lem  19757  dvfsumle  19765  dvfsumabs  19767  dvfsumrlim  19775  ftc1a  19781  ftc1lem6  19785  evlsval  19800  mdegmullem  19861  elply2  19975  plypf1  19991  aalioulem2  20110  aalioulem5  20113  aalioulem6  20114  aaliou  20115  ulmcaulem  20170  ulmcau  20171  ulmss  20173  ulmdvlem3  20178  mtest  20180  itgulm  20184  abelthlem8  20215  abelth  20217  tanord  20300  cxpcn3lem  20491  mcubic  20547  cubic2  20548  dvdsflsumcom  20833  fsumdvdsmul  20840  lgsdchrval  20991  2sqlem9  21017  rplogsumlem2  21039  rpvmasumlem  21041  dchrvmasumlem1  21049  vmalogdivsum2  21092  logsqvma  21096  selberg  21102  selberg4  21115  pntibndlem3  21146  pntlem3  21163  pntleml  21165  padicabv  21184  padicabvf  21185  padicabvcxp  21186  ostth3  21192  cusgrasize2inds  21345  grpolcan  21662  isgrp2d  21664  ghgrp  21797  nvmul0or  21974  sspival  22078  nmosetre  22106  blocnilem  22146  blocni  22147  h2hcau  22323  h2hlm  22324  shsel3  22658  chscllem2  22981  homulcl  23103  adjsym  23177  cnvadj  23236  hhcno  23248  hhcnf  23249  lnopl  23258  unoplin  23264  counop  23265  lnfnl  23275  hmoplin  23286  hmopm  23365  nmcexi  23370  lnconi  23377  riesz3i  23406  leopmuli  23477  leopmul  23478  hstle  23574  mdsl0  23654  mdslmd1lem2  23670  atcvatlem  23729  chirredi  23738  cdj1i  23777  isoun  23923  difioo  23974  gsumpropd2lem  24042  xrge0tsmsd  24045  dya2icoseg2  24415  ballotlemimin  24535  conpcon  24694  cvmliftmolem2  24741  cvmliftlem6  24749  cvmliftlem8  24751  cvmlift2lem10  24771  cvmlift2lem12  24773  relexpsucl  24904  relexpcnv  24905  relexpdm  24907  relexprn  24908  relexpadd  24910  relexpindlem  24911  rtrclreclem.trans  24918  rtrclreclem.min  24919  rtrclind  24921  dedekindle  24960  prodfn0  24994  prodfrec  24995  zprod  25035  fprodeq0  25071  fprodn0  25075  dfon2lem6  25161  poseq  25270  nocvxminlem  25361  nofulllem4  25376  nofulllem5  25377  axpasch  25587  axcontlem7  25616  axcontlem10  25619  ifscgr  25685  brsegle  25749  itg2gt0cn  25953  bddiblnc  25968  ftc1cnnc  25972  comppfsc  26071  neibastop2lem  26073  cover2  26099  filbcmb  26126  fdc  26133  fdc1  26134  seqpo  26135  incsequz  26136  incsequz2  26137  metf1o  26145  lmclim2  26148  geomcau  26149  isbnd2  26176  bndss  26179  equivbnd  26183  ismtybndlem  26199  heibor1lem  26202  rrncmslem  26225  rrnequiv  26228  exidreslem  26236  ghomco  26242  isdrngo3  26259  rngoisocnv  26281  isidlc  26309  idlnegcl  26316  divrngidl  26322  intidl  26323  unichnidl  26325  keridl  26326  igenmin  26358  prnc  26361  ispridlc  26364  prter3  26415  lsmfgcl  26834  kercvrlsm  26843  frlmsslsp  26910  lindfmm  26959  islindf4  26970  hbt  26996  mamuass  27122  cntzsdrg  27172  climinf  27393  cotsqcscsq  27844  glbconxN  29543  atltcvr  29600  3dim1  29632  lvolnle3at  29747  linepsubN  29917  osumclN  30132  pexmidALTN  30143  lhpmatb  30196  cdlemg1idlemN  30737  dihlss  31416  dihglblem5aN  31458  dihatlat  31500
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 178  df-an 361
  Copyright terms: Public domain W3C validator