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  2538  2ralbida  2595  2rexbidva  2597  pofun  4346  tfindsg2  4668  imainss  5112  eqfnfv2  5639  fnex  5757  f1elima  5803  fliftfun  5827  isores2  5846  f1oiso  5864  ovmpt2dxf  5989  grpridd  6076  sorpssuni  6302  sorpssint  6303  oalim  6547  omlim  6548  oaass  6575  omlimcl  6592  omass  6594  oelim2  6609  oeoa  6611  oeoelem  6612  nnaass  6636  omabs  6661  eroveu  6769  sbthlem4  6990  fimaxg  7120  fisupg  7121  fofinf1o  7153  ordtypelem7  7255  hartogs  7275  card2on  7284  unwdomg  7314  wemapwe  7416  dfac5  7771  cfsmolem  7912  isf32lem2  7996  ttukeylem6  8157  ondomon  8201  alephreg  8220  ltexprlem6  8681  recexsrlem  8741  wloglei  9321  recextlem2  9415  fimaxre  9717  creur  9756  uzind3OLD  10123  uz11  10266  xrmaxeq  10524  xrmineq  10525  xaddf  10567  xaddass  10585  xleadd1a  10589  xlt2add  10596  xmullem  10600  xmulgt0  10619  xmulasslem3  10622  xlemul1a  10624  xadddilem  10630  fzrevral  10882  seqcaopr2  11098  expnlbnd2  11248  faclbnd4lem4  11325  shftlem  11579  01sqrex  11751  cau3lem  11854  limsupbnd2  11973  clim2  11994  clim2c  11995  clim0c  11997  rlimresb  12055  2clim  12062  climabs0  12075  climcn1  12081  climcn2  12082  o1rlimmul  12108  climsqz  12130  climsqz2  12131  rlimsqzlem  12138  lo1le  12141  climsup  12159  caucvgrlem2  12163  iseralt  12173  summolem2  12205  fsum2dlem  12249  cvgcmp  12290  cvgcmpce  12292  climfsum  12294  fsumiun  12295  geomulcvg  12348  mertenslem2  12357  mertens  12358  smu01lem  12692  gcdcllem1  12706  gcdmultiplez  12746  dvdssq  12755  coprmdvds2  12798  pclem  12907  pcge0  12930  pcgcd1  12945  prmpwdvds  12967  1arithlem4  12989  4sqlem18  13025  vdwlem10  13053  vdwlem11  13054  ramval  13071  ramub1lem2  13090  ramcl  13092  imasaddfnlem  13446  imasaddflem  13448  imasvscafn  13455  imasleval  13459  ismon2  13653  isepi2  13660  issubc3  13739  cofucl  13778  setcmon  13935  setcepi  13936  ipodrsfi  14282  ipodrsima  14284  isacs3lem  14285  grpidpropd  14415  mhmpropd  14437  mhmima  14456  gsumccat  14480  grplcan  14550  mulgdirlem  14607  subgmulg  14651  issubg4  14654  subgint  14657  cycsubgcl  14659  ssnmz  14675  gastacl  14779  orbsta  14783  galactghm  14799  cntzsubg  14828  odmulg  14885  odbezout  14887  sylow3lem2  14955  lsmsubm  14980  efgsfo  15064  mulgmhm  15143  mulgghm  15144  gsumval3  15207  gsumcllem  15209  gsumpt  15238  gsum2d  15239  gsum2d2  15241  prdsgsum  15245  subgdmdprd  15285  dprd2d2  15295  ablfac1eu  15324  rngpropd  15388  rnglghm  15404  dvdsrpropd  15494  abvpropd  15623  islmodd  15649  lmodprop2d  15703  lsssubg  15730  lsspropd  15790  islmhm2  15811  lmhmima  15820  lsmelval2  15854  lidlsubg  15983  assapropd  16083  asclpropd  16101  psrass1lem  16139  mplcoe1  16225  mplcoe2  16227  mplind  16259  evlslem2  16265  coe1tmmul2  16368  phlpropd  16575  neips  16866  neindisj  16870  ordtrest2lem  16949  lmbrf  17006  lmss  17042  isreg2  17121  lmmo  17124  hauscmplem  17149  2ndcomap  17200  1stcelcls  17203  restlly  17225  islly2  17226  cldllycmp  17237  1stckgenlem  17264  txbas  17278  txbasval  17317  tx1cn  17319  ptpjopn  17322  ptcnp  17332  txnlly  17347  txlm  17358  xkococn  17370  fgabs  17590  fmfnfmlem4  17668  flimcf  17693  hauspwpwf1  17698  fclsbas  17732  fclscf  17736  flimfnfcls  17739  ghmcnp  17813  tgpt0  17817  tsmsxp  17853  isxmet2d  17908  elmopn2  18007  mopni3  18056  blsscls2  18066  metequiv2  18072  metss2lem  18073  met2ndci  18084  metrest  18086  metcnp  18103  metcnp2  18104  metcnpi3  18108  txmetcnp  18109  isngp4  18149  nmolb2d  18243  xrge0tsms  18355  metdsre  18373  metnrmlem3  18381  addcnlem  18384  fsumcn  18390  elcncf2  18410  mulc1cncf  18425  cncfco  18427  cncfmet  18428  bndth  18472  evth  18473  copco  18532  pcopt2  18537  pcoass  18538  pcorevlem  18540  lmmcvg  18703  lmmbrf  18704  iscau4  18721  iscauf  18722  cmetcaulem  18730  iscmet3lem3  18732  iscmet3lem1  18733  causs  18740  equivcfil  18741  lmclim  18744  caubl  18749  caublcls  18750  bcth3  18769  ivthle  18832  ivthle2  18833  ovoliunlem1  18877  ovolicc2lem5  18896  volsuplem  18928  uniioombllem6  18959  dyaddisjlem  18966  dyadmax  18969  volcn  18977  mbfmulc2lem  19018  ismbf3d  19025  mbfsup  19035  mbfinf  19036  mbflim  19039  i1fmullem  19065  itg2seq  19113  itg2uba  19114  itg2splitlem  19119  itg2split  19120  itg2monolem1  19121  ditgsplitlem  19226  ellimc2  19243  ellimc3  19245  limcflf  19247  limcmpt  19249  limcco  19259  c1lip3  19362  lhop1lem  19376  dvfsumle  19384  dvfsumabs  19386  dvfsumrlim  19394  ftc1a  19400  ftc1lem6  19404  evlsval  19419  mdegmullem  19480  elply2  19594  plypf1  19610  aalioulem2  19729  aalioulem5  19732  aalioulem6  19733  aaliou  19734  ulmcaulem  19787  ulmcau  19788  ulmss  19790  ulmdvlem3  19795  mtest  19797  itgulm  19800  abelthlem8  19831  abelth  19833  tanord  19916  cxpcn3lem  20103  mcubic  20159  cubic2  20160  dvdsflsumcom  20444  fsumdvdsmul  20451  lgsdchrval  20602  2sqlem9  20628  rplogsumlem2  20650  rpvmasumlem  20652  dchrvmasumlem1  20660  vmalogdivsum2  20703  logsqvma  20707  selberg  20713  selberg4  20726  pntibndlem3  20757  pntlem3  20774  pntleml  20776  padicabv  20795  padicabvf  20796  padicabvcxp  20797  ostth3  20803  grpolcan  20916  isgrp2d  20918  ghgrp  21051  nvmul0or  21226  sspival  21330  nmosetre  21358  blocnilem  21398  blocni  21399  h2hcau  21575  h2hlm  21576  shsel3  21910  chscllem2  22233  homulcl  22355  adjsym  22429  cnvadj  22488  hhcno  22500  hhcnf  22501  lnopl  22510  unoplin  22516  counop  22517  lnfnl  22527  hmoplin  22538  hmopm  22617  nmcexi  22622  lnconi  22629  riesz3i  22658  leopmuli  22729  leopmul  22730  hstle  22826  mdsl0  22906  mdslmd1lem2  22922  atcvatlem  22981  chirredi  22990  cdj1i  23029  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemimin  23080  isoun  23257  difioo  23290  gsumpropd2lem  23394  xrge0tsmsd  23397  conpcon  23781  cvmliftmolem2  23828  cvmliftlem6  23836  cvmliftlem8  23838  cvmlift2lem10  23858  cvmlift2lem12  23860  relexpsucl  24043  relexpcnv  24044  relexpdm  24047  relexprn  24048  relexpadd  24050  relexpindlem  24051  rtrclreclem.trans  24058  rtrclreclem.min  24059  rtrclind  24061  dedekindle  24098  zprod  24160  dfon2lem6  24215  poseq  24324  nocvxminlem  24415  nofulllem4  24430  nofulllem5  24431  axpasch  24641  axcontlem7  24670  axcontlem10  24673  ifscgr  24739  brsegle  24803  itg2gt0cn  25006  bddiblnc  25021  ftc1cnnc  25025  npincppr  25262  exopcopn  25675  comppfsc  26410  neibastop2lem  26412  cover2  26461  filbcmb  26535  fdc  26558  fdc1  26559  seqpo  26560  incsequz  26561  incsequz2  26562  metf1o  26572  lmclim2  26577  geomcau  26578  isbnd2  26610  bndss  26613  equivbnd  26617  ismtybndlem  26633  heibor1lem  26636  rrncmslem  26659  rrnequiv  26662  exidreslem  26670  ghomco  26676  isdrngo3  26693  rngoisocnv  26715  isidlc  26743  idlnegcl  26750  divrngidl  26756  intidl  26757  unichnidl  26759  keridl  26760  igenmin  26792  prnc  26795  ispridlc  26798  prter3  26853  lsmfgcl  27275  kercvrlsm  27284  frlmsslsp  27351  lindfmm  27400  islindf4  27411  hbt  27437  mamuass  27563  cntzsdrg  27613  climinf  27835  cotsqcscsq  28486  glbconxN  30189  atltcvr  30246  3dim1  30278  lvolnle3at  30393  linepsubN  30563  osumclN  30778  pexmidALTN  30789  lhpmatb  30842  cdlemg1idlemN  31383  dihlss  32062  dihglblem5aN  32104  dihatlat  32146
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