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

Theorem dariiALT 2700
Description: Alternate proof of darii 2699, shorter but using more axioms. This shows how the use of spi 2112 may shorten some proofs of the Aristotelian syllogisms, even though this adds axiom dependencies. Note that spi 2112 is the inference associated with sp 2111, 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 2112 . . 3 (𝜑𝜓)
43anim2i 607 . 2 ((𝜒𝜑) → (𝜒𝜓))
51, 4eximii 1799 1 𝑥(𝜒𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  wal 1505  wex 1742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-12 2106
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator