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  550  wepo  4122  wetrep  4123  fvun1  5271  f1elima  5444  caovimo  5725  supisoti  6482  prarloc  6755  reapmul1  7762  ltmul12a  8005  peano5uzti  8536  eluzp1m1  8723  lbzbi  8782  qreccl  8808  xrlttr  8946  xrltso  8947  elfzodifsumelfzo  9287  ndvdsadd  10475  nn0seqcvgd  10567  isprm3  10644
  Copyright terms: Public domain W3C validator