MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dariiALT Structured version   Visualization version   GIF version

Theorem dariiALT 2664
Description: Alternate proof of darii 2663, shorter but using more axioms. This shows how the use of spi 2182 may shorten some proofs of the Aristotelian syllogisms, even though this adds axiom dependencies. Note that spi 2182 is the inference associated with sp 2181, 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
StepHypRef Expression
1 darii.min . 2 𝑥(𝜒𝜑)
2 darii.maj . . . 4 𝑥(𝜑𝜓)
32spi 2182 . . 3 (𝜑𝜓)
43anim2i 617 . 2 ((𝜒𝜑) → (𝜒𝜓))
51, 4eximii 1834 1 𝑥(𝜒𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wal 1535  wex 1776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator