Theorem stoic1a 1774

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 1774 and stoic1b 1775 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  1775  posn  5720  frsn  5722  relimasn  6054  nssdmovg  7552  iblss  25779  midexlem  28782  colhp  28860  clwwlknon0  30186  xaddeq0  32850  xrge0npcan  33119  elrgspnsubrunlem2  33348  esplyfval3  33755  constrinvcl  33957  madjusmdetlem2  34012  onvf1od  35329  unccur  37883  lindsenlbs  37895  itg2addnclem2  37952  dvasin  37984  ssnel  45432  icccncfext  46274  dirkercncflem1  46490  fourierdlem81  46574  fourierdlem97  46590  prsal  46705  volico2  47028