Theorem stoic1a 1772

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 1772 and stoic1b 1773 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  1773  posn  5717  frsn  5719  relimasn  6045  nssdmovg  7551  iblss  25739  midexlem  28672  colhp  28750  clwwlknon0  30072  xaddeq0  32726  xrge0npcan  33004  elrgspnsubrunlem2  33215  constrinvcl  33756  madjusmdetlem2  33811  onvf1od  35087  unccur  37590  lindsenlbs  37602  itg2addnclem2  37659  dvasin  37691  ssnel  45030  icccncfext  45878  dirkercncflem1  46094  fourierdlem81  46178  fourierdlem97  46194  prsal  46309  volico2  46632