darii

Description: "Darii", one of the syllogisms of Aristotelian logic. All ph is ps , and some ch is ph , therefore some ch is ps . In Aristotelian notation, AII-1: MaP and SiM therefore SiP. For example, given "All rabbits have fur" and "Some pets are rabbits", therefore "Some pets have fur". Example from https://en.wikipedia.org/wiki/Syllogism . See dariiALT for a shorter proof requiring more axioms. (Contributed by David A. Wheeler, 24-Aug-2016) Reduce dependencies on axioms. (Revised by BJ, 16-Sep-2022)

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

Proof

Step	Hyp	Ref	Expression
1		darii.maj	$⊢ \forall x (φ \to ψ)$
2		darii.min	$⊢ \exists x (χ \land φ)$
3		id	$⊢ (φ \to ψ) \to (φ \to ψ)$
4	3	anim2d	$⊢ (φ \to ψ) \to ((χ \land φ) \to (χ \land ψ))$
5	4	alimi	$⊢ \forall x (φ \to ψ) \to \forall x ((χ \land φ) \to (χ \land ψ))$
6	1 5	ax-mp	$⊢ \forall x ((χ \land φ) \to (χ \land ψ))$
7		exim	$⊢ \forall x ((χ \land φ) \to (χ \land ψ)) \to (\exists x (χ \land φ) \to \exists x (χ \land ψ))$
8	6 2 7	mp2	$⊢ \exists x (χ \land ψ)$

Metamath Proof Explorer

Theorem darii

Proof