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

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

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 397

This theorem is referenced by:  stoic1b  1776  posn  5672  frsn  5674  relimasn  5992  nssdmovg  7454  iblss  24969  midexlem  27053  colhp  27131  clwwlknon0  28457  xaddeq0  31076  xrge0npcan  31303  unccur  35760  lindsenlbs  35772  itg2addnclem2  35829  dvasin  35861  ssnel  42588  icccncfext  43428  dirkercncflem1  43644  fourierdlem81  43728  fourierdlem97  43744  prsal  43859  volico2  44179