New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  anassrs GIF version

Theorem anassrs 629
 Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
anassrs.1 ((φ (ψ χ)) → θ)
Assertion
Ref Expression
anassrs (((φ ψ) χ) → θ)

Proof of Theorem anassrs
StepHypRef Expression
1 anassrs.1 . . 3 ((φ (ψ χ)) → θ)
21exp32 588 . 2 (φ → (ψ → (χθ)))
32imp31 421 1 (((φ ψ) χ) → θ)
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator