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  wepo  4361  wetrep  4362  fvun1  5584  f1elima  5776  caovimo  6070  supisoti  7011  prarloc  7504  reapmul1  8554  ltmul12a  8819  peano5uzti  9363  eluzp1m1  9553  lbzbi  9618  qreccl  9644  xrlttr  9797  xrltso  9798  elfzodifsumelfzo  10203  mertensabs  11547  ndvdsadd  11938  nn0seqcvgd  12043  isprm3  12120  ennnfonelemim  12427  grppropd  12898  neissex  13704  lgsval3  14458