Theorem anasss 399

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

Step	Hyp	Ref	Expression
1		anasss.1	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
2	1	exp31 364	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp32 257	1 |- ( ( ph /\ ( ps /\ ch ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  anass  401  anabss3  587  biadanid  618  wepo  4456  wetrep  4457  fvun1  5712  f1elima  5914  caovimo  6216  supisoti  7209  prarloc  7723  reapmul1  8775  ltmul12a  9040  peano5uzti  9588  eluzp1m1  9780  lbzbi  9850  qreccl  9876  xrlttr  10030  xrltso  10031  elfzodifsumelfzo  10447  mertensabs  12116  ndvdsadd  12510  nn0seqcvgd  12631  isprm3  12708  ennnfonelemim  13063  prdsval  13374  grppropd  13618  ghmcmn  13932  neissex  14908  lgsval3  15766  gfsumval  16732