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  575  wepo  4337  wetrep  4338  fvun1  5552  f1elima  5741  caovimo  6035  supisoti  6975  prarloc  7444  reapmul1  8493  ltmul12a  8755  peano5uzti  9299  eluzp1m1  9489  lbzbi  9554  qreccl  9580  xrlttr  9731  xrltso  9732  elfzodifsumelfzo  10136  mertensabs  11478  ndvdsadd  11868  nn0seqcvgd  11973  isprm3  12050  ennnfonelemim  12357  neissex  12805  lgsval3  13559