Theorem stoic1a 1767

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

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

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 206  df-an 395

This theorem is referenced by:  stoic1b  1768  posn  5759  frsn  5761  relimasn  6086  nssdmovg  7600  iblss  25822  midexlem  28616  colhp  28694  clwwlknon0  30023  xaddeq0  32660  xrge0npcan  32906  unccur  37317  lindsenlbs  37329  itg2addnclem2  37386  dvasin  37418  ssnel  44679  icccncfext  45544  dirkercncflem1  45760  fourierdlem81  45844  fourierdlem97  45860  prsal  45975  volico2  46298