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

Theorem anasss 394
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 359 . 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  396  anabss3  557  wepo  4249  wetrep  4250  fvun1  5453  f1elima  5640  caovimo  5930  supisoti  6863  prarloc  7275  reapmul1  8320  ltmul12a  8575  peano5uzti  9110  eluzp1m1  9298  lbzbi  9357  qreccl  9383  xrlttr  9521  xrltso  9522  elfzodifsumelfzo  9918  mertensabs  11246  ndvdsadd  11524  nn0seqcvgd  11618  isprm3  11695  ennnfonelemim  11832  neissex  12229
  Copyright terms: Public domain W3C validator