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

Theorem celarent 2302
Description: "Celarent", one of the syllogisms of Aristotelian logic. No φ is ψ, and all χ is φ, therefore no χ is ψ. (In Aristotelian notation, EAE-1: MeP and SaM therefore SeP.) For example, given the "No reptiles have fur" and "All snakes are reptiles", therefore "No snakes have fur". Example from (Contributed by David A. Wheeler, 24-Aug-2016.) (Revised by David A. Wheeler, 2-Sep-2016.)
Ref Expression
celarent.maj x(φ → ¬ ψ)
celarent.min x(χφ)
Ref Expression
celarent x(χ → ¬ ψ)

Proof of Theorem celarent
StepHypRef Expression
1 celarent.maj . 2 x(φ → ¬ ψ)
2 celarent.min . 2 x(χφ)
31, 2barbara 2301 1 x(χ → ¬ ψ)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1540
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557
This theorem depends on definitions:  df-bi 177  df-an 360
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator