Theorem dariiALT 2654

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

Syntax hints:   → wi 4   ∧ wa 394  ∀wal 1531  ∃wex 1773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774

This theorem is referenced by: (None)