Theorem stoic1a 1775

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 1775 and stoic1b 1776 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 414	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3	2	con3dimp 410	1 ⊢ ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)

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

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 398

This theorem is referenced by:  stoic1b  1776  posn  5762  frsn  5764  relimasn  6084  nssdmovg  7589  iblss  25322  midexlem  27943  colhp  28021  clwwlknon0  29346  xaddeq0  31966  xrge0npcan  32195  unccur  36471  lindsenlbs  36483  itg2addnclem2  36540  dvasin  36572  ssnel  43727  icccncfext  44603  dirkercncflem1  44819  fourierdlem81  44903  fourierdlem97  44919  prsal  45034  volico2  45357