Metamath Proof Explorer


Theorem ferio

Description: "Ferio" ("Ferioque"), one of the syllogisms of Aristotelian logic. No ph is ps , and some ch is ph , therefore some ch is not ps . Instance of darii . In Aristotelian notation, EIO-1: MeP and SiM therefore SoP. For example, given "No homework is fun" and "Some reading is homework", therefore "Some reading is not fun". This is essentially a logical axiom in Aristotelian logic. Example from https://en.wikipedia.org/wiki/Syllogism . (Contributed by David A. Wheeler, 24-Aug-2016)

Ref Expression
Hypotheses ferio.maj
|- A. x ( ph -> -. ps )
ferio.min
|- E. x ( ch /\ ph )
Assertion ferio
|- E. x ( ch /\ -. ps )

Proof

Step Hyp Ref Expression
1 ferio.maj
 |-  A. x ( ph -> -. ps )
2 ferio.min
 |-  E. x ( ch /\ ph )
3 1 2 darii
 |-  E. x ( ch /\ -. ps )