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

Theorem stoic1a 1775
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 1775 and stoic1b 1776 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 414 . 2 (𝜑 → (𝜓𝜃))
32con3dimp 410 1 ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  stoic1b  1776  posn  5762  frsn  5764  relimasn  6084  nssdmovg  7589  iblss  25322  midexlem  27974  colhp  28052  clwwlknon0  29377  xaddeq0  31997  xrge0npcan  32226  unccur  36519  lindsenlbs  36531  itg2addnclem2  36588  dvasin  36620  ssnel  43775  icccncfext  44651  dirkercncflem1  44867  fourierdlem81  44951  fourierdlem97  44967  prsal  45082  volico2  45405
  Copyright terms: Public domain W3C validator