Theorem stoic1a 1774

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

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

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 207  df-an 396

This theorem is referenced by:  stoic1b  1775  posn  5711  frsn  5713  relimasn  6045  nssdmovg  7542  iblss  25766  midexlem  28768  colhp  28846  clwwlknon0  30172  xaddeq0  32835  xrge0npcan  33104  elrgspnsubrunlem2  33332  esplyfval3  33732  constrinvcl  33932  madjusmdetlem2  33987  onvf1od  35303  unccur  37806  lindsenlbs  37818  itg2addnclem2  37875  dvasin  37907  ssnel  45355  icccncfext  46198  dirkercncflem1  46414  fourierdlem81  46498  fourierdlem97  46514  prsal  46629  volico2  46952