Theorem camestres

"Camestres", one of the syllogisms of Aristotelian logic. All \( \varphi \) is \( \psi \), and no \( \chi \) is \( \psi \), therefore no \( \chi \) is \( \varphi \). In Aristotelian notation, AEE-2: PaM and SeM therefore SeP. (Contributed by David A. Wheeler, 28-Aug-2016.) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022.)

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