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

Theorem stoic1a 1838
Description: Stoic logic Thema 1 (part a).

The first thema of the four Stoic logic themata, in its basic form, was:

"When from two (assertibles) a third follows, then from either of them together with the contradictory of the conclusion the contradictory of the other follows." (Apuleius Int. 209.9-14), see [Bobzien] p. 117 and https://plato.stanford.edu/entries/logic-ancient/

We will represent thema 1 as two very similar rules stoic1a 1838 and stoic1b 1839 to represent each side. (Contributed by David A. Wheeler, 16-Feb-2019.) (Proof shortened by Wolf Lammen, 21-May-2020.)

Hypothesis
Ref Expression
stoic1.1 ((𝜑𝜓) → 𝜃)
Assertion
Ref Expression
stoic1a ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)

Proof of Theorem stoic1a
StepHypRef Expression
1 stoic1.1 . . 3 ((𝜑𝜓) → 𝜃)
21ex 449 . 2 (𝜑 → (𝜓𝜃))
32con3dimp 456 1 ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  stoic1b  1839  posn  5336  frsn  5338  relimasn  5638  nssdmovg  6973  iblss  23762  midexlem  25778  colhp  25853  clwwlknon0  27232  xaddeq0  29819  xrge0npcan  29995  unccur  33697  lindsenlbs  33709  itg2addnclem2  33767  dvasin  33801  ssnel  39695  icccncfext  40595  dirkercncflem1  40815  fourierdlem81  40899  fourierdlem97  40915  volico2  41353
  Copyright terms: Public domain W3C validator