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

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

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  580  wepo  4344  wetrep  4345  fvun1  5562  f1elima  5752  caovimo  6046  supisoti  6987  prarloc  7465  reapmul1  8514  ltmul12a  8776  peano5uzti  9320  eluzp1m1  9510  lbzbi  9575  qreccl  9601  xrlttr  9752  xrltso  9753  elfzodifsumelfzo  10157  mertensabs  11500  ndvdsadd  11890  nn0seqcvgd  11995  isprm3  12072  ennnfonelemim  12379  grppropd  12724  neissex  12959  lgsval3  13713