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

Theorem dariiALT 2728
 Description: Alternate proof of darii 2727, 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.)
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 2181 . . 3 (𝜑𝜓)
43anim2i 619 . 2 ((𝜒𝜑) → (𝜒𝜓))
51, 4eximii 1838 1 𝑥(𝜒𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1536  ∃wex 1781 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator