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

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