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  4406  wetrep  4407  fvun1  5645  f1elima  5842  caovimo  6140  supisoti  7112  prarloc  7616  reapmul1  8668  ltmul12a  8933  peano5uzti  9481  eluzp1m1  9672  lbzbi  9737  qreccl  9763  xrlttr  9917  xrltso  9918  elfzodifsumelfzo  10330  mertensabs  11848  ndvdsadd  12242  nn0seqcvgd  12363  isprm3  12440  ennnfonelemim  12795  prdsval  13105  grppropd  13349  ghmcmn  13663  neissex  14637  lgsval3  15495