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

Theorem stoic1a 1687
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 1687 and stoic1b 1688 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 448 . 2 (𝜑 → (𝜓𝜃))
32con3dimp 455 1 ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  stoic1b  1688  posn  5096  frsn  5098  relimasn  5390  nssdmovg  6687  iblss  23290  midexlem  25301  colhp  25376  xaddeq0  28709  xrge0npcan  28827  unccur  32361  lindsenlbs  32373  itg2addnclem2  32431  dvasin  32465  ssnel  38026  icccncfext  38573  dirkercncflem1  38796  fourierdlem81  38880  fourierdlem97  38896  volico2  39331
  Copyright terms: Public domain W3C validator