Theorem stoic1a 1772

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 1772 and stoic1b 1773 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 415	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3	2	con3dimp 411	1 ⊢ ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)

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

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 209  df-an 399

This theorem is referenced by:  stoic1b  1773  posn  5640  frsn  5642  relimasn  5955  nssdmovg  7333  iblss  24408  midexlem  26481  colhp  26559  clwwlknon0  27875  xaddeq0  30480  xrge0npcan  30685  unccur  34879  lindsenlbs  34891  itg2addnclem2  34948  dvasin  34982  ssnel  41308  icccncfext  42176  dirkercncflem1  42395  fourierdlem81  42479  fourierdlem97  42495  prsal  42610  volico2  42930