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  5737  frsn  5739  relimasn  6083  nssdmovg  7603  lindsenlbs  22157  iblss  26125  midexlem  29164  colhp  29248  plngrotlem1  29265  prlngplngtr  29437  clwwlknon0  30684  xaddeq0  33345  xrge0npcan  33581  elrgspnsubrunlem2  33809  drnglring  34024  esplyfval3  34204  constrinvcl  34405  madjusmdetlem2  34460  onvf1od  35886  unccur  38526  itg2addnclem2  38590  dvasin  38622  ssnel  46059  icccncfext  46896  dirkercncflem1  47112  fourierdlem81  47196  fourierdlem97  47212  prsal  47327  volico2  47650  indprmfz  48714