Theorem stoic1a 1800

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 1800 and stoic1b 1801 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 ⊢ ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)

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

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 210  df-an 401

This theorem is referenced by:  stoic1b  1801  posn  5751  frsn  5753  relimasn  6091  nssdmovg  7596  iblss  25947  midexlem  28949  colhp  29031  plngrotlem1  29047  prlngplngtr  29185  clwwlknon0  30414  xaddeq0  33068  xrge0npcan  33310  elrgspnsubrunlem2  33538  drnglring  33752  esplyfval3  33932  constrinvcl  34133  madjusmdetlem2  34188  onvf1od  35549  unccur  38202  lindsenlbs  38214  itg2addnclem2  38271  dvasin  38303  ssnel  45715  icccncfext  46553  dirkercncflem1  46769  fourierdlem81  46853  fourierdlem97  46869  prsal  46984  volico2  47307  indprmfz  48331