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

Theorem thema1a 1579
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 1579 and thema1b 1580 to represent each side. (Contributed by David A. Wheeler, 16-Feb-2019.)

Hypothesis
Ref Expression
thema1.1  |-  ( (
ph  /\  ps )  ->  th )
Assertion
Ref Expression
thema1a  |-  ( (
ph  /\  -.  th )  ->  -.  ps )

Proof of Theorem thema1a
StepHypRef Expression
1 thema1.1 . . . . . 6  |-  ( (
ph  /\  ps )  ->  th )
21con3i 135 . . . . 5  |-  ( -. 
th  ->  -.  ( ph  /\ 
ps ) )
3 ianor 488 . . . . 5  |-  ( -.  ( ph  /\  ps ) 
<->  ( -.  ph  \/  -.  ps ) )
42, 3sylib 196 . . . 4  |-  ( -. 
th  ->  ( -.  ph  \/  -.  ps ) )
54anim2i 569 . . 3  |-  ( (
ph  /\  -.  th )  ->  ( ph  /\  ( -.  ph  \/  -.  ps ) ) )
6 orcom 387 . . . 4  |-  ( ( ( ph  /\  -.  ph )  \/  ( ph  /\ 
-.  ps ) )  <->  ( ( ph  /\  -.  ps )  \/  ( ph  /\  -.  ph ) ) )
7 andi 862 . . . 4  |-  ( (
ph  /\  ( -.  ph  \/  -.  ps )
)  <->  ( ( ph  /\ 
-.  ph )  \/  ( ph  /\  -.  ps )
) )
8 pm3.24 877 . . . . 5  |-  -.  ( ph  /\  -.  ph )
98biorfi 407 . . . 4  |-  ( (
ph  /\  -.  ps )  <->  ( ( ph  /\  -.  ps )  \/  ( ph  /\  -.  ph )
) )
106, 7, 93bitr4i 277 . . 3  |-  ( (
ph  /\  ( -.  ph  \/  -.  ps )
)  <->  ( ph  /\  -.  ps ) )
115, 10sylib 196 . 2  |-  ( (
ph  /\  -.  th )  ->  ( ph  /\  -.  ps ) )
1211simprd 463 1  |-  ( (
ph  /\  -.  th )  ->  -.  ps )
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  1580
  Copyright terms: Public domain W3C validator