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  616  wepo  4450  wetrep  4451  fvun1  5700  f1elima  5897  caovimo  6199  supisoti  7177  prarloc  7690  reapmul1  8742  ltmul12a  9007  peano5uzti  9555  eluzp1m1  9746  lbzbi  9811  qreccl  9837  xrlttr  9991  xrltso  9992  elfzodifsumelfzo  10407  mertensabs  12048  ndvdsadd  12442  nn0seqcvgd  12563  isprm3  12640  ennnfonelemim  12995  prdsval  13306  grppropd  13550  ghmcmn  13864  neissex  14839  lgsval3  15697