Theorem anasss 396

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 361	. 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  398  anabss3  574  wepo  4276  wetrep  4277  fvun1  5480  f1elima  5667  caovimo  5957  supisoti  6890  prarloc  7304  reapmul1  8350  ltmul12a  8611  peano5uzti  9152  eluzp1m1  9342  lbzbi  9401  qreccl  9427  xrlttr  9574  xrltso  9575  elfzodifsumelfzo  9971  mertensabs  11299  ndvdsadd  11617  nn0seqcvgd  11711  isprm3  11788  ennnfonelemim  11926  neissex  12323