Theorem anasss 391

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 356	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp32 253	1 |- ( ( ph /\ ( ps /\ ch ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  anass  393  anabss3  549  wepo  4114  wetrep  4115  fvun1  5260  f1elima  5433  caovimo  5714  supisoti  6423  prarloc  6693  reapmul1  7695  ltmul12a  7938  peano5uzti  8455  eluzp1m1  8642  lbzbi  8701  qreccl  8727  xrlttr  8870  xrltso  8871  elfzodifsumelfzo  9210  ndvdsadd  10331  nn0seqcvgd  10423  isprm3  10500