Theorem calemes

"Calemes", one of the syllogisms of Aristotelian logic. All \( \varphi \) is \( \psi \), and no \( \psi \) is \( \chi \), therefore no \( \chi \) is \( \varphi \). 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.)

Hypotheses
calemes.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
calemes.min
\( \vdash \forall x \, (\psi \rightarrow \neg \chi) \)
Conclusion
\( \vdash \forall x \, (\chi \rightarrow \neg \varphi) \)
Proof
l0
calemes.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
l1
calemes.min
\( \vdash \forall x \, (\psi \rightarrow \neg \chi) \)
con2
alimi _
\( \vdash \forall x \, (\psi \rightarrow \neg \chi) \rightarrow \forall x \, (\chi \rightarrow \neg \psi) \)
ax-mp l1 _
\( \vdash \forall x \, (\chi \rightarrow \neg \psi) \)
camestres l0 _