Theorem anasss 399

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  anass  401  anabss3  585  biadanid  614  wepo  4394  wetrep  4395  fvun1  5627  f1elima  5820  caovimo  6117  supisoti  7076  prarloc  7570  reapmul1  8622  ltmul12a  8887  peano5uzti  9434  eluzp1m1  9625  lbzbi  9690  qreccl  9716  xrlttr  9870  xrltso  9871  elfzodifsumelfzo  10277  mertensabs  11702  ndvdsadd  12096  nn0seqcvgd  12209  isprm3  12286  ennnfonelemim  12641  grppropd  13149  ghmcmn  13457  neissex  14401  lgsval3  15259