Theorem dariiALT

Description: Alternate proof of darii , shorter but using more axioms. This shows how the use of spi may shorten some proofs of the Aristotelian syllogisms, even though this adds axiom dependencies. Note that spi is the inference associated with sp , which corresponds to the axiom (T) of modal logic. (Contributed by David A. Wheeler, 27-Aug-2016) Added precisions on axiom usage. (Revised by BJ, 27-Sep-2022) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	darii.maj	⊢ ∀ 𝑥 ( 𝜑 → 𝜓 )
	darii.min	⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜑 )
Assertion	dariiALT	⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		darii.maj	⊢ ∀ 𝑥 ( 𝜑 → 𝜓 )
2		darii.min	⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜑 )
3	1	spi	⊢ ( 𝜑 → 𝜓 )
4	3	anim2i	⊢ ( ( 𝜒 ∧ 𝜑 ) → ( 𝜒 ∧ 𝜓 ) )
5	2 4	eximii	⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜓 )