Theorem cesare

"Cesare", one of the syllogisms of Aristotelian logic. No \( \varphi \) is \( \psi \), and all \( \chi \) is \( \psi \), therefore no \( \chi \) is \( \varphi \). In Aristotelian notation, EAE-2: PeM and SaM therefore SeP. Related to celarent. (Contributed by David A. Wheeler, 27-Aug-2016.) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022.)

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