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  2595  2ralbida  2653  2rexbidva  2655  dfimafn  5366  funimass4  5368  eqfnfv2  5393  f1elima  5474  isores2  5493  isomin  5496  f1oiso  5499  weds  5938