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

Theorem anasss 628
Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
anasss.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
anasss  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )

Proof of Theorem anasss
StepHypRef Expression
1 anasss.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
21exp31 587 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 422 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  anass  630  anabss3  796  f1elima  5803  fnfvof  6106  oecl  6552  oaass  6575  oen0  6600  oeworde  6607  omabs  6661  suppr  7235  oiiniseg  7264  cardinfima  7740  fpwwe2lem12  8279  ltmul12a  9628  uzindOLD  10122  uzind3OLD  10123  eluzp1m1  10267  lbzbi  10322  qreccl  10352  xrlttr  10490  quoremnn0  10976  incexc2  12313  mertens  12358  ndvdsadd  12623  nn0seqcvgd  12756  isprm3  12783  pcval  12913  prdsval  13371  evlfcl  14012  frgpup1  15100  frgpup3lem  15102  gsumval3  15207  gsumzoppg  15232  ablfaclem2  15337  gsumdixp  15408  psrass1lem  16139  psrass1  16166  neissex  16880  tx1stc  17360  kqreglem1  17448  xpstopnlem1  17516  alexsublem  17754  icoopnst  18453  iocopnst  18454  volcn  18977  mbflimsup  19037  mbflim  19039  itg1addlem4  19070  itg1addlem5  19071  itg1climres  19085  limcflf  19247  dvcobr  19311  dvcnvlem  19339  dvfsumge  19385  mdegmullem  19480  plyeq0lem  19608  plypf1  19610  mbfulm  19798  fsumdvdscom  20441  muinv  20449  logfaclbnd  20477  logexprlim  20480  dchrinv  20516  lgsval3  20569  rpvmasum2  20677  dchrisum0lem1  20681  dchrisum0  20685  selberg  20713  selberg3lem1  20722  selberg34r  20736  pntsval2  20741  grpoidinvlem4  20890  ipblnfi  21450  shmodsi  21984  eighmorth  22560  kbass5  22716  kbass6  22717  dmdmd  22896  atom1d  22949  mdsymlem2  23000  mdsymlem3  23001  mdsymlem4  23002  mdsymlem5  23003  ofrn  23221  esumcst  23451  rescon  23792  nocvxminlem  24415  nobndlem6  24422  colinearalg  24610  axeuclid  24663  axcontlem2  24665  axcontlem7  24670  itg2gt0cn  25006  cover2  26461  indexa  26515  filbcmb  26535  seqpo  26560  incsequz  26561  isbnd2  26610  ghomco  26676  unichnidl  26759  isfldidl  26796  frlmgsum  27335  unxpwdom3  27359  dihvalc  32045  dihvalb  32049
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