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  4289  wetrep  4290  fvun1  5495  f1elima  5682  caovimo  5972  supisoti  6905  prarloc  7335  reapmul1  8381  ltmul12a  8642  peano5uzti  9183  eluzp1m1  9373  lbzbi  9435  qreccl  9461  xrlttr  9611  xrltso  9612  elfzodifsumelfzo  10009  mertensabs  11338  ndvdsadd  11664  nn0seqcvgd  11758  isprm3  11835  ennnfonelemim  11973  neissex  12373