This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fesapo

Description: "Fesapo", one of the syllogisms of Aristotelian logic. No ph is ps , all ps is ch , and ps exist, therefore some ch is not ph . In Aristotelian notation, EAO-4: PeM and MaS therefore SoP. (Contributed by David A. Wheeler, 28-Aug-2016) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

Ref Expression
Hypotheses fesapo.maj ⊢ ∀ x φ → ¬ ψ
fesapo.min ⊢ ∀ x ψ → χ
fesapo.e ⊢ ∃ x ψ
Assertion fesapo ⊢ ∃ x χ ∧ ¬ φ

Proof

Step Hyp Ref Expression
1 fesapo.maj ⊢ ∀ x φ → ¬ ψ
2 fesapo.min ⊢ ∀ x ψ → χ
3 fesapo.e ⊢ ∃ x ψ
4 con2 ⊢ φ → ¬ ψ → ψ → ¬ φ
5 4 alimi ⊢ ∀ x φ → ¬ ψ → ∀ x ψ → ¬ φ
6 1 5 ax-mp ⊢ ∀ x ψ → ¬ φ
7 6 2 3 felapton ⊢ ∃ x χ ∧ ¬ φ