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

Theorem stoic1a 1772
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 1772 and stoic1b 1773 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 412 . 2 (𝜑 → (𝜓𝜃))
32con3dimp 408 1 ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  stoic1b  1773  posn  5771  frsn  5773  relimasn  6103  nssdmovg  7615  iblss  25840  midexlem  28700  colhp  28778  clwwlknon0  30112  xaddeq0  32757  xrge0npcan  33025  elrgspnsubrunlem2  33252  madjusmdetlem2  33827  unccur  37610  lindsenlbs  37622  itg2addnclem2  37679  dvasin  37711  ssnel  45048  icccncfext  45902  dirkercncflem1  46118  fourierdlem81  46202  fourierdlem97  46218  prsal  46333  volico2  46656
  Copyright terms: Public domain W3C validator