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  4395  wetrep  4396  fvun1  5628  f1elima  5821  caovimo  6118  supisoti  7077  prarloc  7572  reapmul1  8624  ltmul12a  8889  peano5uzti  9436  eluzp1m1  9627  lbzbi  9692  qreccl  9718  xrlttr  9872  xrltso  9873  elfzodifsumelfzo  10279  mertensabs  11704  ndvdsadd  12098  nn0seqcvgd  12219  isprm3  12296  ennnfonelemim  12651  grppropd  13159  ghmcmn  13467  neissex  14411  lgsval3  15269