![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dariiALT | Structured version Visualization version GIF version |
Description: Alternate proof of darii 2654, shorter but using more axioms. This shows how the use of spi 2169 may shorten some proofs of the Aristotelian syllogisms, even though this adds axiom dependencies. Note that spi 2169 is the inference associated with sp 2168, 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 |
---|---|
darii.maj | ⊢ ∀𝑥(𝜑 → 𝜓) |
darii.min | ⊢ ∃𝑥(𝜒 ∧ 𝜑) |
Ref | Expression |
---|---|
dariiALT | ⊢ ∃𝑥(𝜒 ∧ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | darii.min | . 2 ⊢ ∃𝑥(𝜒 ∧ 𝜑) | |
2 | darii.maj | . . . 4 ⊢ ∀𝑥(𝜑 → 𝜓) | |
3 | 2 | spi 2169 | . . 3 ⊢ (𝜑 → 𝜓) |
4 | 3 | anim2i 616 | . 2 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓)) |
5 | 1, 4 | eximii 1831 | 1 ⊢ ∃𝑥(𝜒 ∧ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∀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 2163 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1774 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |