This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cesaro

Description: "Cesaro", one of the syllogisms of Aristotelian logic. No ph is ps , all ch is ps , and ch exist, therefore some ch is not ph . In Aristotelian notation, EAO-2: PeM and SaM therefore SoP. (Contributed by David A. Wheeler, 28-Aug-2016) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

	Ref	Expression
Hypotheses	cesaro.maj	$⊢ \forall x (φ \to \neg ψ)$
	cesaro.min	$⊢ \forall x (χ \to ψ)$
	cesaro.e	$⊢ \exists x χ$
Assertion	cesaro	$⊢ \exists x (χ \land \neg φ)$

Proof

Step	Hyp	Ref	Expression
1		cesaro.maj	$⊢ \forall x (φ \to \neg ψ)$
2		cesaro.min	$⊢ \forall x (χ \to ψ)$
3		cesaro.e	$⊢ \exists x χ$
4	1 2	cesare	$⊢ \forall x (χ \to \neg φ)$
5	3 4	barbarilem	$⊢ \exists x (χ \land \neg φ)$