This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Other axiomatizations related to classical predicate calculus Aristotelian logic: Assertic syllogisms festino
Description: "Festino", one of the syllogisms of Aristotelian logic. No ph is
ps , and some ch is ps , therefore some ch is not
ph . In Aristotelian notation, EIO-2: PeM and SiM therefore SoP.
(Contributed by David A. Wheeler , 25-Nov-2016) Reduce dependencies on
axioms. (Revised by BJ , 16-Sep-2022)
Ref
Expression
Hypotheses
festino.maj |- A. x ( ph -> -. ps )
festino.min |- E. x ( ch /\ ps )
Assertion
festino |- E. x ( ch /\ -. ph )
Proof
Step
Hyp
Ref
Expression
1
festino.maj |- A. x ( ph -> -. ps )
2
festino.min |- E. x ( ch /\ ps )
3
con2 |- ( ( ph -> -. ps ) -> ( ps -> -. ph ) )
4
3
anim2d |- ( ( ph -> -. ps ) -> ( ( ch /\ ps ) -> ( ch /\ -. ph ) ) )
5
4
alimi |- ( A. x ( ph -> -. ps ) -> A. x ( ( ch /\ ps ) -> ( ch /\ -. ph ) ) )
6
1 5
ax-mp |- A. x ( ( ch /\ ps ) -> ( ch /\ -. ph ) )
7
exim |- ( A. x ( ( ch /\ ps ) -> ( ch /\ -. ph ) ) -> ( E. x ( ch /\ ps ) -> E. x ( ch /\ -. ph ) ) )
8
6 2 7
mp2 |- E. x ( ch /\ -. ph )