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

Theorem stoic1a 1605
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 1605 and stoic1b 1606 to represent each side. (Contributed by David A. Wheeler, 16-Feb-2019.)

Hypothesis
Ref Expression
stoic1.1
Assertion
Ref Expression
stoic1a

Proof of Theorem stoic1a
StepHypRef Expression
1 stoic1.1 . . . . . 6
21con3i 135 . . . . 5
3 ianor 488 . . . . 5
42, 3sylib 196 . . . 4
54anim2i 569 . . 3
6 orcom 387 . . . 4
7 andi 867 . . . 4
8 pm3.24 882 . . . . 5
98biorfi 407 . . . 4
106, 7, 93bitr4i 277 . . 3
115, 10sylib 196 . 2
1211simprd 463 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  \/wo 368  /\wa 369
This theorem is referenced by:  stoic1b  1606  posn  5073  frsn  5075  relimasn  5365  nssdmovg  6457  iblss  22211  midexlem  24069  xaddeq0  27573  xrge0npcan  27684  itg2addnclem2  30067  dvasin  30103  ssnel  31422  icccncfext  31690  dirkercncflem1  31885  fourierdlem81  31970  fourierdlem97  31986
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 185  df-or 370  df-an 371
  Copyright terms: Public domain W3C validator