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

Theorem anassrs 648
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 605 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 432 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  anass  649  mpanr1  683  pm2.61ddan  790  pm2.61dda  791  anass1rs  805  anabss5  812  anabss7  817  pm2.61da2ne  2685  2ralbida  2749  2rexbidva  2751  copsexg  4571  pofun  4652  imainss  5247  eqfnfv2  5793  fnex  5939  f1elima  5971  fliftfun  6000  isores2  6019  f1oiso  6037  ovmpt2dxf  6211  grpridd  6298  sorpssuni  6364  sorpssint  6365  tfindsg2  6467  oalim  6964  omlim  6965  oaass  6992  omlimcl  7009  omass  7011  oelim2  7026  oeoa  7028  oeoelem  7029  nnaass  7053  omabs  7078  eroveu  7187  sbthlem4  7416  fimaxg  7551  fisupg  7552  fofinf1o  7584  ordtypelem7  7730  hartogs  7750  card2on  7761  unwdomg  7791  wemapwe  7920  wemapweOLD  7921  dfac5  8290  cfsmolem  8431  isf32lem2  8515  ttukeylem6  8675  ondomon  8719  alephreg  8738  ltexprlem6  9202  recexsrlem  9262  dedekindle  9526  wloglei  9864  recextlem2  9959  fimaxre  10269  creur  10308  uzind3OLD  10729  uz11  10875  xrmaxeq  11143  xrmineq  11144  xaddf  11186  xaddass  11204  xleadd1a  11208  xlt2add  11215  xmullem  11219  xmulgt0  11238  xmulasslem3  11241  xlemul1a  11243  xadddilem  11249  fzrevral  11536  seqcaopr2  11834  expnlbnd2  11987  faclbnd4lem4  12064  shftlem  12549  01sqrex  12731  cau3lem  12834  limsupbnd2  12953  clim2  12974  clim2c  12975  clim0c  12977  rlimresb  13035  2clim  13042  climabs0  13055  climcn1  13061  climcn2  13062  o1rlimmul  13088  climsqz  13110  climsqz2  13111  rlimsqzlem  13118  lo1le  13121  climsup  13139  caucvgrlem2  13144  iseralt  13154  summolem2  13185  fsum2dlem  13229  cvgcmp  13271  cvgcmpce  13273  climfsum  13275  fsumiun  13276  geomulcvg  13328  mertenslem2  13337  mertens  13338  smu01lem  13673  gcdcllem1  13687  gcdmultiplez  13727  dvdssq  13736  coprmdvds2  13781  pclem  13897  pcge0  13920  pcgcd1  13935  prmpwdvds  13957  1arithlem4  13979  4sqlem18  14015  vdwlem10  14043  vdwlem11  14044  ramval  14061  ramub1lem2  14080  ramcl  14082  imasaddfnlem  14458  imasaddflem  14460  imasvscafn  14467  imasleval  14471  ismon2  14665  isepi2  14672  issubc3  14751  cofucl  14790  setcmon  14947  setcepi  14948  ipodrsfi  15325  ipodrsima  15327  isacs3lem  15328  grpidpropd  15439  mhmpropd  15462  mhmima  15482  gsumpropd2lem  15496  gsumccat  15510  grplcan  15581  mulgdirlem  15642  subgmulg  15686  issubg4  15691  subgint  15696  cycsubgcl  15698  ssnmz  15714  gastacl  15818  orbsta  15822  cntzsubg  15845  galactghm  15899  odmulg  16048  odbezout  16050  sylow3lem2  16118  lsmsubm  16143  efgsfo  16227  mulgmhm  16306  mulgghm  16307  gsumval3OLD  16373  gsumval3  16376  gsumcllem  16377  gsumcllemOLD  16378  gsumpt  16443  gsumptOLD  16444  gsum2d  16451  gsum2dOLD  16452  gsum2d2  16454  prdsgsum  16459  prdsgsumOLD  16460  subgdmdprd  16519  dprd2d2  16531  ablfac1eu  16562  srglmhm  16622  srgrmhm  16623  rngpropd  16664  rnglghm  16681  dvdsrpropd  16776  abvpropd  16905  islmodd  16932  lmodprop2d  16985  lsssubg  17015  lsspropd  17075  islmhm2  17096  lmhmima  17105  lsmelval2  17143  lidlsubg  17274  assapropd  17375  asclpropd  17393  psrass1lem  17424  mplcoe1  17521  mplcoe2  17524  mplcoe2OLD  17525  mplind  17559  evlslem2  17572  evlsval  17580  coe1tmmul2  17704  phlpropd  18059  frlmsslsp  18198  frlmsslspOLD  18199  lindfmm  18231  islindf4  18242  mamuass  18281  mavmulass  18335  mdetuni0  18402  mdetmul  18404  neips  18692  neindisj  18696  ordtrest2lem  18782  lmbrf  18839  lmss  18877  isreg2  18956  lmmo  18959  hauscmplem  18984  bwth  18988  2ndcomap  19037  1stcelcls  19040  restlly  19062  islly2  19063  cldllycmp  19074  1stckgenlem  19101  txbas  19115  txbasval  19154  tx1cn  19157  ptpjopn  19160  ptcnp  19170  txnlly  19185  txlm  19196  xkococn  19208  fgabs  19427  fmfnfmlem4  19505  flimcf  19530  hauspwpwf1  19535  fclsbas  19569  fclscf  19573  flimfnfcls  19576  ghmcnp  19660  tgpt0  19664  tsmsxp  19704  isxmet2d  19877  elmopn2  19995  mopni3  20044  blsscls2  20054  metequiv2  20060  metss2lem  20061  met2ndci  20072  metrest  20074  metcnp  20091  metcnp2  20092  metcnpi3  20096  txmetcnp  20097  isngp4  20178  nmolb2d  20272  xrge0tsms  20386  metdsre  20404  metnrmlem3  20412  addcnlem  20415  fsumcn  20421  elcncf2  20441  mulc1cncf  20456  cncfco  20458  cncfmet  20459  bndth  20505  evth  20506  copco  20565  pcopt2  20570  pcoass  20571  pcorevlem  20573  lmmcvg  20747  lmmbrf  20748  iscau4  20765  iscauf  20766  cmetcaulem  20774  iscmet3lem3  20776  iscmet3lem1  20777  causs  20784  equivcfil  20785  lmclim  20788  caubl  20793  caublcls  20794  bcth3  20817  ivthle  20915  ivthle2  20916  ovoliunlem1  20960  ovolicc2lem5  20979  volsuplem  21011  uniioombllem6  21043  dyaddisjlem  21050  dyadmax  21053  volcn  21061  mbfmulc2lem  21100  ismbf3d  21107  mbfsup  21117  mbfinf  21118  mbflim  21121  i1fmullem  21147  itg2seq  21195  itg2uba  21196  itg2splitlem  21201  itg2split  21202  itg2monolem1  21203  ditgsplitlem  21310  ellimc2  21327  ellimc3  21329  limcflf  21331  limcmpt  21333  limcco  21343  c1lip3  21446  lhop1lem  21460  dvfsumle  21468  dvfsumabs  21470  dvfsumrlim  21478  ftc1a  21484  ftc1lem6  21488  mdegmullem  21524  elply2  21639  plypf1  21655  aalioulem2  21774  aalioulem5  21777  aalioulem6  21778  aaliou  21779  ulmcaulem  21834  ulmcau  21835  ulmss  21837  ulmdvlem3  21842  mtest  21844  itgulm  21848  abelthlem8  21879  abelth  21881  tanord  21969  cxpcn3lem  22160  mcubic  22217  cubic2  22218  dvdsflsumcom  22503  fsumdvdsmul  22510  lgsdchrval  22661  2sqlem9  22687  rplogsumlem2  22709  rpvmasumlem  22711  dchrvmasumlem1  22719  vmalogdivsum2  22762  logsqvma  22766  selberg  22772  selberg4  22785  pntibndlem3  22816  pntlem3  22833  pntleml  22835  padicabv  22854  padicabvf  22855  padicabvcxp  22856  ostth3  22862  axpasch  23138  axcontlem7  23167  axcontlem10  23170  cusgrasize2inds  23336  grpolcan  23671  isgrp2d  23673  ghgrp  23806  nvmul0or  23983  sspival  24087  nmosetre  24115  blocnilem  24155  blocni  24156  h2hcau  24332  h2hlm  24333  shsel3  24669  chscllem2  24992  homulcl  25114  adjsym  25188  cnvadj  25247  hhcno  25259  hhcnf  25260  lnopl  25269  unoplin  25275  counop  25276  lnfnl  25286  hmoplin  25297  hmopm  25376  nmcexi  25381  lnconi  25388  riesz3i  25417  leopmuli  25488  leopmul  25489  hstle  25585  mdsl0  25665  mdslmd1lem2  25681  atcvatlem  25740  chirredi  25749  cdj1i  25788  isoun  25948  difioo  26023  xrge0tsmsd  26204  pstmxmet  26276  ordtrest2NEWlem  26304  dya2icoseg2  26645  eulerpartlemgc  26697  eulerpartlemgvv  26711  eulerpartlemgh  26713  eulerpartlemgs2  26715  ballotlemimin  26840  signstfvneq0  26925  conpcon  27076  cvmliftmolem2  27123  cvmliftlem6  27131  cvmliftlem8  27133  cvmlift2lem10  27153  cvmlift2lem12  27155  relexpsucl  27285  relexpcnv  27286  relexpdm  27288  relexprn  27289  relexpadd  27291  relexpindlem  27292  rtrclreclem.trans  27299  rtrclreclem.min  27300  rtrclind  27302  prodfn0  27360  prodfrec  27361  zprod  27401  fprodeq0  27437  fprodn0  27441  fprod2dlem  27442  dfon2lem6  27552  poseq  27665  nocvxminlem  27782  nofulllem4  27797  nofulllem5  27798  ifscgr  28026  brsegle  28090  finixpnum  28367  fin2solem  28368  fin2so  28369  heicant  28379  itg2gt0cn  28400  bddiblnc  28415  ftc1cnnc  28419  ftc1anclem5  28424  ftc1anclem6  28425  ftc1anclem7  28426  ftc1anc  28428  comppfsc  28532  neibastop2lem  28534  cover2  28560  filbcmb  28587  fdc  28594  fdc1  28595  seqpo  28596  incsequz  28597  incsequz2  28598  metf1o  28604  lmclim2  28607  geomcau  28608  isbnd2  28635  bndss  28638  equivbnd  28642  ismtybndlem  28658  heibor1lem  28661  rrncmslem  28684  rrnequiv  28687  exidreslem  28695  ghomco  28701  isdrngo3  28718  rngoisocnv  28740  isidlc  28768  idlnegcl  28775  divrngidl  28781  intidl  28782  unichnidl  28784  keridl  28785  igenmin  28817  prnc  28820  ispridlc  28823  prter3  28980  lsmfgcl  29380  kercvrlsm  29389  unxpwdom3  29401  hbt  29439  cntzsdrg  29512  climinf  29732  2spotdisj  30607  ovmpt2rdxf  30681  cotsqcscsq  30986  glbconxN  32862  atltcvr  32919  3dim1  32951  lvolnle3at  33066  linepsubN  33236  osumclN  33451  pexmidALTN  33462  lhpmatb  33515  cdlemg1idlemN  34056  dihlss  34735  dihglblem5aN  34777  dihatlat  34819
  Copyright terms: Public domain W3C validator