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 416	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3	2	con3dimp 412	1 ⊢ ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)

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

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 210  df-an 400

This theorem is referenced by:  stoic1b  1775  posn  5601  frsn  5603  relimasn  5919  nssdmovg  7310  iblss  24408  midexlem  26486  colhp  26564  clwwlknon0  27878  xaddeq0  30503  xrge0npcan  30728  unccur  35040  lindsenlbs  35052  itg2addnclem2  35109  dvasin  35141  ssnel  41674  icccncfext  42529  dirkercncflem1  42745  fourierdlem81  42829  fourierdlem97  42845  prsal  42960  volico2  43280