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  5745  frsn  5747  relimasn  6085  nssdmovg  7599  lindsenlbs  22065  iblss  26034  midexlem  29041  colhp  29125  plngrotlem1  29142  prlngplngtr  29302  clwwlknon0  30549  xaddeq0  33211  xrge0npcan  33447  elrgspnsubrunlem2  33675  drnglring  33889  esplyfval3  34069  constrinvcl  34270  madjusmdetlem2  34325  onvf1od  35691  unccur  38344  itg2addnclem2  38408  dvasin  38440  ssnel  45864  icccncfext  46702  dirkercncflem1  46918  fourierdlem81  47002  fourierdlem97  47018  prsal  47133  volico2  47456  indprmfz  48520