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

Step	Hyp	Ref	Expression
1		stoic1.1	. . . . . 6
2	1	con3i 135	. . . . 5
3		ianor 488	. . . . 5
4	2, 3	sylib 196	. . . 4
5	4	anim2i 569	. . 3
6		orcom 387	. . . 4
7		andi 867	. . . 4
8		pm3.24 882	. . . . 5
9	8	biorfi 407	. . . 4
10	6, 7, 9	3bitr4i 277	. . 3
11	5, 10	sylib 196	. 2
12	11	simprd 463	1

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