ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anasss Unicode version

Theorem anasss 397
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 362 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 255 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  anass  399  anabss3  580  wepo  4344  wetrep  4345  fvun1  5562  f1elima  5752  caovimo  6046  supisoti  6987  prarloc  7465  reapmul1  8514  ltmul12a  8776  peano5uzti  9320  eluzp1m1  9510  lbzbi  9575  qreccl  9601  xrlttr  9752  xrltso  9753  elfzodifsumelfzo  10157  mertensabs  11500  ndvdsadd  11890  nn0seqcvgd  11995  isprm3  12072  ennnfonelemim  12379  grppropd  12724  neissex  12959  lgsval3  13713
  Copyright terms: Public domain W3C validator