MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  stoic1a Structured version   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 1607 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  |-  ( (
ph  /\  ps )  ->  th )
Assertion
Ref Expression
stoic1a  |-  ( (
ph  /\  -.  th )  ->  -.  ps )

Proof of Theorem stoic1a
StepHypRef Expression
1 stoic1.1 . . . 4  |-  ( (
ph  /\  ps )  ->  th )
21ex 434 . . 3  |-  ( ph  ->  ( ps  ->  th )
)
32con3d 133 . 2  |-  ( ph  ->  ( -.  th  ->  -. 
ps ) )
43imp 429 1  |-  ( (
ph  /\  -.  th )  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ 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-an 371
This theorem is referenced by:  stoic1b  1607  posn  5077  frsn  5079  relimasn  5370  nssdmovg  6456  iblss  22337  midexlem  24195  xaddeq0  27730  xrge0npcan  27844  itg2addnclem2  30272  dvasin  30308  ssnel  31625  icccncfext  31893  dirkercncflem1  32088  fourierdlem81  32173  fourierdlem97  32189
  Copyright terms: Public domain W3C validator