Theorem stoic1a 1801

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 1801 and stoic1b 1802 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 417	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3	2	con3dimp 413	1 ⊢ ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  stoic1b  1802  posn  5746  frsn  5748  relimasn  6086  nssdmovg  7594  iblss  25975  midexlem  28980  colhp  29063  plngrotlem1  29080  prlngplngtr  29220  clwwlknon0  30455  xaddeq0  33109  xrge0npcan  33349  elrgspnsubrunlem2  33577  drnglring  33791  esplyfval3  33971  constrinvcl  34172  madjusmdetlem2  34227  onvf1od  35599  unccur  38282  lindsenlbs  38294  itg2addnclem2  38351  dvasin  38383  ssnel  45791  icccncfext  46629  dirkercncflem1  46845  fourierdlem81  46929  fourierdlem97  46945  prsal  47060  volico2  47383  indprmfz  48410