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  5702  f1elima  5903  caovimo  6205  supisoti  7188  prarloc  7701  reapmul1  8753  ltmul12a  9018  peano5uzti  9566  eluzp1m1  9758  lbzbi  9823  qreccl  9849  xrlttr  10003  xrltso  10004  elfzodifsumelfzo  10419  mertensabs  12064  ndvdsadd  12458  nn0seqcvgd  12579  isprm3  12656  ennnfonelemim  13011  prdsval  13322  grppropd  13566  ghmcmn  13880  neissex  14855  lgsval3  15713