Theorem dariiALT 2750

Description: Alternate proof of darii 2749, shorter but using more axioms. This shows how the use of spi 2182 may shorten some proofs of the Aristotelian syllogisms, even though this adds axiom dependencies. Note that spi 2182 is the inference associated with sp 2181, 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 2182	. . 3 ⊢ (𝜑 → 𝜓)
4	3	anim2i 618	. 2 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))
5	1, 4	eximii 1836	1 ⊢ ∃𝑥(𝜒 ∧ 𝜓)

Syntax hints:   → wi 4   ∧ wa 398  ∀wal 1534  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-12 2176

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780

This theorem is referenced by: (None)