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

Theorem thema1a 1589
 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 thema1a 1589 and thema1b 1590 to represent each side. (Contributed by David A. Wheeler, 16-Feb-2019.)
Hypothesis
Ref Expression
thema1.1
Assertion
Ref Expression
thema1a

Proof of Theorem thema1a
StepHypRef Expression
1 thema1.1 . . . . . 6
21con3i 135 . . . . 5
3 ianor 488 . . . . 5
42, 3sylib 196 . . . 4
54anim2i 569 . . 3
6 orcom 387 . . . 4
7 andi 865 . . . 4
8 pm3.24 880 . . . . 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 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 This theorem is referenced by:  thema1b  1590
 Copyright terms: Public domain W3C validator