Theorem stoic1a 1838

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 1838 and stoic1b 1839 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 449	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3	2	con3dimp 456	1 ⊢ ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)

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

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 385

This theorem is referenced by:  stoic1b  1839  posn  5336  frsn  5338  relimasn  5638  nssdmovg  6973  iblss  23762  midexlem  25778  colhp  25853  clwwlknon0  27232  xaddeq0  29819  xrge0npcan  29995  unccur  33697  lindsenlbs  33709  itg2addnclem2  33767  dvasin  33801  ssnel  39695  icccncfext  40595  dirkercncflem1  40815  fourierdlem81  40899  fourierdlem97  40915  volico2  41353