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

Theorem stoic1a 1694
 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 1694 and stoic1b 1695 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 450 . 2 (𝜑 → (𝜓𝜃))
32con3dimp 457 1 ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384 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 386 This theorem is referenced by:  stoic1b  1695  posn  5158  frsn  5160  relimasn  5457  nssdmovg  6781  iblss  23511  midexlem  25521  colhp  25596  xaddeq0  29402  xrge0npcan  29521  unccur  33063  lindsenlbs  33075  itg2addnclem2  33133  dvasin  33167  ssnel  38726  icccncfext  39435  dirkercncflem1  39657  fourierdlem81  39741  fourierdlem97  39757  volico2  40192
 Copyright terms: Public domain W3C validator