Theorem stoic1a 1805

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 1805 and stoic1b 1806 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 418	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3	2	con3dimp 414	1 ⊢ ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)

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

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 402

This theorem is used by:  stoic1b  1806  posn  5733  frsn  5735  relimasn  6075  nssdmovg  7591  lindsenlbs  22118  iblss  26086  midexlem  29097  colhp  29181  plngrotlem1  29198  prlngplngtr  29370  clwwlknon0  30617  xaddeq0  33278  xrge0npcan  33514  elrgspnsubrunlem2  33742  drnglring  33957  esplyfval3  34137  constrinvcl  34338  madjusmdetlem2  34393  onvf1od  35811  unccur  38446  itg2addnclem2  38510  dvasin  38542  ssnel  45981  icccncfext  46819  dirkercncflem1  47035  fourierdlem81  47119  fourierdlem97  47135  prsal  47250  volico2  47573  indprmfz  48637