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  4390  wetrep  4391  fvun1  5623  f1elima  5816  caovimo  6112  supisoti  7069  prarloc  7563  reapmul1  8614  ltmul12a  8879  peano5uzti  9425  eluzp1m1  9616  lbzbi  9681  qreccl  9707  xrlttr  9861  xrltso  9862  elfzodifsumelfzo  10268  mertensabs  11680  ndvdsadd  12072  nn0seqcvgd  12179  isprm3  12256  ennnfonelemim  12581  grppropd  13089  ghmcmn  13397  neissex  14333  lgsval3  15134