|   | 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 2664, shorter but using more axioms. This shows how the use of spi 2183 may shorten some proofs of the Aristotelian syllogisms, even though this adds axiom dependencies. Note that spi 2183 is the inference associated with sp 2182, 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 2183 | . . 3 ⊢ (𝜑 → 𝜓) | 
| 4 | 3 | anim2i 617 | . 2 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓)) | 
| 5 | 1, 4 | eximii 1836 | 1 ⊢ ∃𝑥(𝜒 ∧ 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∀wal 1537 ∃wex 1778 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-12 2176 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 | 
| This theorem is referenced by: (None) | 
| Copyright terms: Public domain | W3C validator |