Theorem stoic1a 1780

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

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

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 209  df-an 398

This theorem is referenced by:  stoic1b  1781  posn  5707  frsn  5709  relimasn  6044  nssdmovg  7542  iblss  25794  midexlem  28782  colhp  28860  clwwlknon0  30185  xaddeq0  32849  xrge0npcan  33103  elrgspnsubrunlem2  33333  drnglring  33587  esplyfval3  33768  constrinvcl  33969  madjusmdetlem2  34024  onvf1od  35350  unccur  37985  lindsenlbs  37997  itg2addnclem2  38054  dvasin  38086  ssnel  45506  icccncfext  46344  dirkercncflem1  46560  fourierdlem81  46644  fourierdlem97  46660  prsal  46775  volico2  47098  indprmfz  48122