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  5712  frsn  5714  relimasn  6046  nssdmovg  7544  iblss  25786  midexlem  28778  colhp  28856  clwwlknon0  30182  xaddeq0  32845  xrge0npcan  33099  elrgspnsubrunlem2  33328  esplyfval3  33735  constrinvcl  33937  madjusmdetlem2  33992  onvf1od  35309  unccur  37944  lindsenlbs  37956  itg2addnclem2  38013  dvasin  38045  ssnel  45498  icccncfext  46339  dirkercncflem1  46555  fourierdlem81  46639  fourierdlem97  46655  prsal  46770  volico2  47093  indprmfz  48111