Metamath Proof Explorer


Theorem calemes

Description: "Calemes", one of the syllogisms of Aristotelian logic. All ph is ps , and no ps is ch , therefore no ch is ph . In Aristotelian notation, AEE-4: PaM and MeS therefore SeP. (Contributed by David A. Wheeler, 28-Aug-2016) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

Ref Expression
Hypotheses calemes.maj
|- A. x ( ph -> ps )
calemes.min
|- A. x ( ps -> -. ch )
Assertion calemes
|- A. x ( ch -> -. ph )

Proof

Step Hyp Ref Expression
1 calemes.maj
 |-  A. x ( ph -> ps )
2 calemes.min
 |-  A. x ( ps -> -. ch )
3 con2
 |-  ( ( ps -> -. ch ) -> ( ch -> -. ps ) )
4 3 alimi
 |-  ( A. x ( ps -> -. ch ) -> A. x ( ch -> -. ps ) )
5 2 4 ax-mp
 |-  A. x ( ch -> -. ps )
6 1 5 camestres
 |-  A. x ( ch -> -. ph )