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  587  biadanid  618  wepo  4486  wetrep  4487  fvun1  5750  f1elima  5954  caovimo  6258  supisoti  7316  prarloc  7836  reapmul1  8889  ltmul12a  9156  peano5uzti  9709  eluzp1m1  9901  lbzbi  9971  qreccl  9997  xrlttr  10152  xrltso  10153  elfzodifsumelfzo  10573  mertensabs  12254  ndvdsadd  12648  nn0seqcvgd  12769  isprm3  12846  ennnfonelemim  13265  grppropd  13778  ghmcmn  14086  gfsumval  14108  prdsval  14121  neissex  15162  lgsval3  16023