MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  celarent Structured version   Visualization version   GIF version

Theorem celarent 2721
Description: "Celarent", one of the syllogisms of Aristotelian logic. No 𝜑 is 𝜓, and all 𝜒 is 𝜑, therefore no 𝜒 is 𝜓. Instance of barbara 2720. 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.)
Ref Expression
celarent.maj 𝑥(𝜑 → ¬ 𝜓)
celarent.min 𝑥(𝜒𝜑)
Ref Expression
celarent 𝑥(𝜒 → ¬ 𝜓)

Proof of Theorem celarent
StepHypRef Expression
1 celarent.maj . 2 𝑥(𝜑 → ¬ 𝜓)
2 celarent.min . 2 𝑥(𝜒𝜑)
31, 2barbara 2720 1 𝑥(𝜒 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1651
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905
This theorem depends on definitions:  df-bi 199  df-an 386
This theorem is referenced by:  cesare  2729  camestres  2731
  Copyright terms: Public domain W3C validator