![]() |
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 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.) |
Ref | Expression |
---|---|
darii.maj | ⊢ ∀𝑥(𝜑 → 𝜓) |
darii.min | ⊢ ∃𝑥(𝜒 ∧ 𝜑) |
Ref | Expression |
---|---|
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 ⊢ ∃𝑥(𝜒 ∧ 𝜓) |
Colors of variables: wff setvar class |
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) |
Copyright terms: Public domain | W3C validator |