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

Theorem stoic1a 1774
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 1774 and stoic1b 1775 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 416 . 2 (𝜑 → (𝜓𝜃))
32con3dimp 412 1 ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  stoic1b  1775  posn  5625  frsn  5627  relimasn  5940  nssdmovg  7325  iblss  24414  midexlem  26492  colhp  26570  clwwlknon0  27884  xaddeq0  30491  xrge0npcan  30716  unccur  34986  lindsenlbs  34998  itg2addnclem2  35055  dvasin  35087  ssnel  41595  icccncfext  42456  dirkercncflem1  42672  fourierdlem81  42756  fourierdlem97  42772  prsal  42887  volico2  43207
  Copyright terms: Public domain W3C validator