Theorem anassrs 629

Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
anassrs.1	|- ((ph /\ (ps /\ ch)) -> th)

Assertion

Ref	Expression
anassrs	|- (((ph /\ ps) /\ ch) -> th)

Proof of Theorem anassrs

Step	Hyp	Ref	Expression
1		anassrs.1	. . 3 |- ((ph /\ (ps /\ ch)) -> th)
2	1	exp32 588	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp31 421	1 |- (((ph /\ ps) /\ ch) -> th)

Syntax hints:   -> wi 4   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  anass  630  mpanr1  664  pm2.61ddan  767  pm2.61dda  768  anass1rs  782  anabss5  789  anabss7  794  pm2.61da2ne  2596  2ralbida  2654  2rexbidva  2656  dfimafn  5367  funimass4  5369  eqfnfv2  5394  f1elima  5475  isores2  5494  isomin  5497  f1oiso  5500  weds  5939