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  585  biadanid  614  wepo  4395  wetrep  4396  fvun1  5630  f1elima  5823  caovimo  6121  supisoti  7085  prarloc  7587  reapmul1  8639  ltmul12a  8904  peano5uzti  9451  eluzp1m1  9642  lbzbi  9707  qreccl  9733  xrlttr  9887  xrltso  9888  elfzodifsumelfzo  10294  mertensabs  11719  ndvdsadd  12113  nn0seqcvgd  12234  isprm3  12311  ennnfonelemim  12666  prdsval  12975  grppropd  13219  ghmcmn  13533  neissex  14485  lgsval3  15343