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

Metamath Proof Explorer

Theorem calemos

Description: "Calemos", one of the syllogisms of Aristotelian logic. All ph is ps (PaM), no ps is ch (MeS), and ch exist, therefore some ch is not ph (SoP). In Aristotelian notation, AEO-4: PaM and MeS therefore SoP. (Contributed by David A. Wheeler, 28-Aug-2016) Shorten and reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

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

Proof

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