Theorem stoic1a 1794

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 1794 and stoic1b 1795 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 416	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3	2	con3dimp 412	1 ⊢ ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)

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

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 400

This theorem is referenced by:  stoic1b  1795  posn  5735  frsn  5737  relimasn  6076  nssdmovg  7580  iblss  25869  midexlem  28867  colhp  28945  plngrotlem1  28996  clwwlknon0  30297  xaddeq0  32957  xrge0npcan  33200  elrgspnsubrunlem2  33431  drnglring  33690  esplyfval3  33871  constrinvcl  34072  madjusmdetlem2  34127  onvf1od  35454  unccur  38107  lindsenlbs  38119  itg2addnclem2  38176  dvasin  38208  ssnel  45628  icccncfext  46466  dirkercncflem1  46682  fourierdlem81  46766  fourierdlem97  46782  prsal  46897  volico2  47220  indprmfz  48244