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  575  wepo  4319  wetrep  4320  fvun1  5534  f1elima  5723  caovimo  6014  supisoti  6954  prarloc  7423  reapmul1  8470  ltmul12a  8731  peano5uzti  9272  eluzp1m1  9462  lbzbi  9525  qreccl  9551  xrlttr  9702  xrltso  9703  elfzodifsumelfzo  10100  mertensabs  11434  ndvdsadd  11822  nn0seqcvgd  11918  isprm3  11995  ennnfonelemim  12164  neissex  12576
  Copyright terms: Public domain W3C validator