Theorem stoic1a 1779

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 1779 and stoic1b 1780 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  1780  posn  5672  frsn  5674  relimasn  5990  nssdmovg  7446  iblss  24965  midexlem  27049  colhp  27127  clwwlknon0  28451  xaddeq0  31070  xrge0npcan  31297  unccur  35754  lindsenlbs  35766  itg2addnclem2  35823  dvasin  35855  ssnel  42556  icccncfext  43397  dirkercncflem1  43613  fourierdlem81  43697  fourierdlem97  43713  prsal  43828  volico2  44148