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  4452  wetrep  4453  fvun1  5706  f1elima  5907  caovimo  6209  supisoti  7198  prarloc  7711  reapmul1  8763  ltmul12a  9028  peano5uzti  9576  eluzp1m1  9768  lbzbi  9838  qreccl  9864  xrlttr  10018  xrltso  10019  elfzodifsumelfzo  10434  mertensabs  12085  ndvdsadd  12479  nn0seqcvgd  12600  isprm3  12677  ennnfonelemim  13032  prdsval  13343  grppropd  13587  ghmcmn  13901  neissex  14876  lgsval3  15734