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  4407  wetrep  4408  fvun1  5647  f1elima  5844  caovimo  6142  supisoti  7114  prarloc  7618  reapmul1  8670  ltmul12a  8935  peano5uzti  9483  eluzp1m1  9674  lbzbi  9739  qreccl  9765  xrlttr  9919  xrltso  9920  elfzodifsumelfzo  10332  mertensabs  11881  ndvdsadd  12275  nn0seqcvgd  12396  isprm3  12473  ennnfonelemim  12828  prdsval  13138  grppropd  13382  ghmcmn  13696  neissex  14670  lgsval3  15528