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

Theorem anasss 391
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 356 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 253 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  anass  393  anabss3  552  wepo  4186  wetrep  4187  fvun1  5370  f1elima  5552  caovimo  5838  supisoti  6703  prarloc  7060  reapmul1  8070  ltmul12a  8319  peano5uzti  8852  eluzp1m1  9040  lbzbi  9099  qreccl  9125  xrlttr  9263  xrltso  9264  elfzodifsumelfzo  9608  mertensabs  10927  ndvdsadd  11205  nn0seqcvgd  11297  isprm3  11374
  Copyright terms: Public domain W3C validator