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 2665, shorter but using more axioms. This shows how the use of spi 2181 may shorten some proofs of the Aristotelian syllogisms, even though this adds axiom dependencies. Note that spi 2181 is the inference associated with sp 2180, 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 2181 | . . 3 ⊢ (𝜑 → 𝜓) |
4 | 3 | anim2i 620 | . 2 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓)) |
5 | 1, 4 | eximii 1844 | 1 ⊢ ∃𝑥(𝜒 ∧ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∀wal 1541 ∃wex 1787 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-12 2175 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |