Theorem stoic1a 1697

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 1697 and stoic1b 1698 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

Step	Hyp	Ref	Expression
1		stoic1.1	. . 3 |- ( ( ph /\ ps ) -> th )
2	1	ex 450	. 2 |- ( ph -> ( ps -> th ) )
3	2	con3dimp 457	1 |- ( ( ph /\ -. th ) -> -. ps )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  stoic1b  1698  posn  5187  frsn  5189  relimasn  5488  nssdmovg  6816  iblss  23571  midexlem  25587  colhp  25662  xaddeq0  29518  xrge0npcan  29694  unccur  33392  lindsenlbs  33404  itg2addnclem2  33462  dvasin  33496  ssnel  39204  icccncfext  40100  dirkercncflem1  40320  fourierdlem81  40404  fourierdlem97  40420  volico2  40855