Theorem dariiALT 2692

Description: Alternate proof of darii 2691, shorter but using more axioms. This shows how the use of spi 2219 may shorten some proofs of the Aristotelian syllogisms, even though this adds axiom dependencies. Note that spi 2219 is the inference associated with sp 2218, 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.)

Hypotheses

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

Assertion

Ref	Expression
dariiALT	⊢ ∃𝑥(𝜒 ∧ 𝜓)

Proof of Theorem dariiALT

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

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1558  ∃wex 1799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-12 2212

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800

This theorem is referenced by: (None)