ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  celarent GIF version

Theorem celarent 2041
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 2040 1 𝑥(𝜒 → ¬ 𝜓)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wal 1283
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator