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

Theorem celarent 2552
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 𝑥(𝜑 → ¬ 𝜓)
celarent.min 𝑥(𝜒𝜑)
Ref Expression
celarent 𝑥(𝜒 → ¬ 𝜓)

Proof of Theorem celarent
StepHypRef Expression
1 celarent.maj . 2 𝑥(𝜑 → ¬ 𝜓)
2 celarent.min . 2 𝑥(𝜒𝜑)
31, 2barbara 2551 1 𝑥(𝜒 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728
This theorem depends on definitions:  df-bi 196  df-an 385
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator