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	⊢ ∀ 𝑥 ( 𝜑 → ¬ 𝜓 )
	ferio.min	⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜑 )
Assertion	ferio	⊢ ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		ferio.maj	⊢ ∀ 𝑥 ( 𝜑 → ¬ 𝜓 )
2		ferio.min	⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜑 )
3	1 2	darii	⊢ ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜓 )