Theorem stoic1a 1773

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 1773 and stoic1b 1774 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	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Assertion

Ref	Expression
stoic1a	⊢ ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)

Proof of Theorem stoic1a

Step	Hyp	Ref	Expression
1		stoic1.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
2	1	ex 412	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3	2	con3dimp 408	1 ⊢ ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  stoic1b  1774  posn  5710  frsn  5712  relimasn  6044  nssdmovg  7540  iblss  25762  midexlem  28764  colhp  28842  clwwlknon0  30168  xaddeq0  32833  xrge0npcan  33102  elrgspnsubrunlem2  33330  esplyfval3  33730  constrinvcl  33930  madjusmdetlem2  33985  onvf1od  35301  unccur  37800  lindsenlbs  37812  itg2addnclem2  37869  dvasin  37901  ssnel  45284  icccncfext  46127  dirkercncflem1  46343  fourierdlem81  46427  fourierdlem97  46443  prsal  46558  volico2  46881