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  2685  2ralbida  2746  2rexbidva  2748  pofun  4522  tfindsg2  4844  imainss  5290  eqfnfv2  5831  fnex  5964  f1elima  6012  fliftfun  6037  isores2  6056  f1oiso  6074  ovmpt2dxf  6202  grpridd  6290  sorpssuni  6534  sorpssint  6535  oalim  6779  omlim  6780  oaass  6807  omlimcl  6824  omass  6826  oelim2  6841  oeoa  6843  oeoelem  6844  nnaass  6868  omabs  6893  eroveu  7002  sbthlem4  7223  fimaxg  7357  fisupg  7358  fofinf1o  7390  ordtypelem7  7496  hartogs  7516  card2on  7525  unwdomg  7555  wemapwe  7657  dfac5  8014  cfsmolem  8155  isf32lem2  8239  ttukeylem6  8399  ondomon  8443  alephreg  8462  ltexprlem6  8923  recexsrlem  8983  wloglei  9564  recextlem2  9658  fimaxre  9960  creur  9999  uzind3OLD  10370  uz11  10513  xrmaxeq  10772  xrmineq  10773  xaddf  10815  xaddass  10833  xleadd1a  10837  xlt2add  10844  xmullem  10848  xmulgt0  10867  xmulasslem3  10870  xlemul1a  10872  xadddilem  10878  fzrevral  11136  seqcaopr2  11364  expnlbnd2  11515  faclbnd4lem4  11592  shftlem  11888  01sqrex  12060  cau3lem  12163  limsupbnd2  12282  clim2  12303  clim2c  12304  clim0c  12306  rlimresb  12364  2clim  12371  climabs0  12384  climcn1  12390  climcn2  12391  o1rlimmul  12417  climsqz  12439  climsqz2  12440  rlimsqzlem  12447  lo1le  12450  climsup  12468  caucvgrlem2  12473  iseralt  12483  summolem2  12515  fsum2dlem  12559  cvgcmp  12600  cvgcmpce  12602  climfsum  12604  fsumiun  12605  geomulcvg  12658  mertenslem2  12667  mertens  12668  smu01lem  13002  gcdcllem1  13016  gcdmultiplez  13056  dvdssq  13065  coprmdvds2  13108  pclem  13217  pcge0  13240  pcgcd1  13255  prmpwdvds  13277  1arithlem4  13299  4sqlem18  13335  vdwlem10  13363  vdwlem11  13364  ramval  13381  ramub1lem2  13400  ramcl  13402  imasaddfnlem  13758  imasaddflem  13760  imasvscafn  13767  imasleval  13771  ismon2  13965  isepi2  13972  issubc3  14051  cofucl  14090  setcmon  14247  setcepi  14248  ipodrsfi  14594  ipodrsima  14596  isacs3lem  14597  grpidpropd  14727  mhmpropd  14749  mhmima  14768  gsumccat  14792  grplcan  14862  mulgdirlem  14919  subgmulg  14963  issubg4  14966  subgint  14969  cycsubgcl  14971  ssnmz  14987  gastacl  15091  orbsta  15095  galactghm  15111  cntzsubg  15140  odmulg  15197  odbezout  15199  sylow3lem2  15267  lsmsubm  15292  efgsfo  15376  mulgmhm  15455  mulgghm  15456  gsumval3  15519  gsumcllem  15521  gsumpt  15550  gsum2d  15551  gsum2d2  15553  prdsgsum  15557  subgdmdprd  15597  dprd2d2  15607  ablfac1eu  15636  rngpropd  15700  rnglghm  15716  dvdsrpropd  15806  abvpropd  15935  islmodd  15961  lmodprop2d  16011  lsssubg  16038  lsspropd  16098  islmhm2  16119  lmhmima  16128  lsmelval2  16162  lidlsubg  16291  assapropd  16391  asclpropd  16409  psrass1lem  16447  mplcoe1  16533  mplcoe2  16535  mplind  16567  evlslem2  16573  coe1tmmul2  16673  phlpropd  16891  neips  17182  neindisj  17186  ordtrest2lem  17272  lmbrf  17329  lmss  17367  isreg2  17446  lmmo  17449  hauscmplem  17474  2ndcomap  17526  1stcelcls  17529  restlly  17551  islly2  17552  cldllycmp  17563  1stckgenlem  17590  txbas  17604  txbasval  17643  tx1cn  17646  ptpjopn  17649  ptcnp  17659  txnlly  17674  txlm  17685  xkococn  17697  fgabs  17916  fmfnfmlem4  17994  flimcf  18019  hauspwpwf1  18024  fclsbas  18058  fclscf  18062  flimfnfcls  18065  ghmcnp  18149  tgpt0  18153  tsmsxp  18189  isxmet2d  18362  elmopn2  18480  mopni3  18529  blsscls2  18539  metequiv2  18545  metss2lem  18546  met2ndci  18557  metrest  18559  metcnp  18576  metcnp2  18577  metcnpi3  18581  txmetcnp  18582  isngp4  18663  nmolb2d  18757  xrge0tsms  18870  metdsre  18888  metnrmlem3  18896  addcnlem  18899  fsumcn  18905  elcncf2  18925  mulc1cncf  18940  cncfco  18942  cncfmet  18943  bndth  18988  evth  18989  copco  19048  pcopt2  19053  pcoass  19054  pcorevlem  19056  lmmcvg  19219  lmmbrf  19220  iscau4  19237  iscauf  19238  cmetcaulem  19246  iscmet3lem3  19248  iscmet3lem1  19249  causs  19256  equivcfil  19257  lmclim  19260  caubl  19265  caublcls  19266  bcth3  19289  ivthle  19358  ivthle2  19359  ovoliunlem1  19403  ovolicc2lem5  19422  volsuplem  19454  uniioombllem6  19485  dyaddisjlem  19492  dyadmax  19495  volcn  19503  mbfmulc2lem  19542  ismbf3d  19549  mbfsup  19559  mbfinf  19560  mbflim  19563  i1fmullem  19589  itg2seq  19637  itg2uba  19638  itg2splitlem  19643  itg2split  19644  itg2monolem1  19645  ditgsplitlem  19752  ellimc2  19769  ellimc3  19771  limcflf  19773  limcmpt  19775  limcco  19785  c1lip3  19888  lhop1lem  19902  dvfsumle  19910  dvfsumabs  19912  dvfsumrlim  19920  ftc1a  19926  ftc1lem6  19930  evlsval  19945  mdegmullem  20006  elply2  20120  plypf1  20136  aalioulem2  20255  aalioulem5  20258  aalioulem6  20259  aaliou  20260  ulmcaulem  20315  ulmcau  20316  ulmss  20318  ulmdvlem3  20323  mtest  20325  itgulm  20329  abelthlem8  20360  abelth  20362  tanord  20445  cxpcn3lem  20636  mcubic  20692  cubic2  20693  dvdsflsumcom  20978  fsumdvdsmul  20985  lgsdchrval  21136  2sqlem9  21162  rplogsumlem2  21184  rpvmasumlem  21186  dchrvmasumlem1  21194  vmalogdivsum2  21237  logsqvma  21241  selberg  21247  selberg4  21260  pntibndlem3  21291  pntlem3  21308  pntleml  21310  padicabv  21329  padicabvf  21330  padicabvcxp  21331  ostth3  21337  cusgrasize2inds  21491  grpolcan  21826  isgrp2d  21828  ghgrp  21961  nvmul0or  22138  sspival  22242  nmosetre  22270  blocnilem  22310  blocni  22311  h2hcau  22487  h2hlm  22488  shsel3  22822  chscllem2  23145  homulcl  23267  adjsym  23341  cnvadj  23400  hhcno  23412  hhcnf  23413  lnopl  23422  unoplin  23428  counop  23429  lnfnl  23439  hmoplin  23450  hmopm  23529  nmcexi  23534  lnconi  23541  riesz3i  23570  leopmuli  23641  leopmul  23642  hstle  23738  mdsl0  23818  mdslmd1lem2  23834  atcvatlem  23893  chirredi  23902  cdj1i  23941  isoun  24094  difioo  24150  gsumpropd2lem  24225  xrge0tsmsd  24228  pstmxmet  24297  dya2icoseg2  24633  ballotlemimin  24768  conpcon  24927  cvmliftmolem2  24974  cvmliftlem6  24982  cvmliftlem8  24984  cvmlift2lem10  25004  cvmlift2lem12  25006  relexpsucl  25137  relexpcnv  25138  relexpdm  25140  relexprn  25141  relexpadd  25143  relexpindlem  25144  rtrclreclem.trans  25151  rtrclreclem.min  25152  rtrclind  25154  dedekindle  25193  prodfn0  25227  prodfrec  25228  zprod  25268  fprodeq0  25304  fprodn0  25308  fprod2dlem  25309  dfon2lem6  25420  poseq  25533  nocvxminlem  25650  nofulllem4  25665  nofulllem5  25666  axpasch  25885  axcontlem7  25914  axcontlem10  25917  ifscgr  25983  brsegle  26047  heicant  26253  itg2gt0cn  26274  bddiblnc  26289  ftc1cnnc  26293  ftc1anclem5  26298  ftc1anclem6  26299  ftc1anclem7  26300  ftc1anc  26302  comppfsc  26401  neibastop2lem  26403  cover2  26429  filbcmb  26456  fdc  26463  fdc1  26464  seqpo  26465  incsequz  26466  incsequz2  26467  metf1o  26475  lmclim2  26478  geomcau  26479  isbnd2  26506  bndss  26509  equivbnd  26513  ismtybndlem  26529  heibor1lem  26532  rrncmslem  26555  rrnequiv  26558  exidreslem  26566  ghomco  26572  isdrngo3  26589  rngoisocnv  26611  isidlc  26639  idlnegcl  26646  divrngidl  26652  intidl  26653  unichnidl  26655  keridl  26656  igenmin  26688  prnc  26691  ispridlc  26694  prter3  26745  lsmfgcl  27163  kercvrlsm  27172  frlmsslsp  27239  lindfmm  27288  islindf4  27299  hbt  27325  mamuass  27451  cntzsdrg  27501  climinf  27722  2spotdisj  28524  cotsqcscsq  28579  glbconxN  30249  atltcvr  30306  3dim1  30338  lvolnle3at  30453  linepsubN  30623  osumclN  30838  pexmidALTN  30849  lhpmatb  30902  cdlemg1idlemN  31443  dihlss  32122  dihglblem5aN  32164  dihatlat  32206
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