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  5742  frsn  5744  relimasn  6094  nssdmovg  7624  lindsenlbs  22184  iblss  26152  midexlem  29191  colhp  29275  plngrotlem1  29292  prlngplngtr  29464  clwwlknon0  30711  xaddeq0  33412  xrge0npcan  33648  elrgspnsubrunlem2  33876  drnglring  34091  esplyfval3  34271  constrinvcl  34472  madjusmdetlem2  34527  ecscottd  35843  onvf1od  36034  unccur  38717  itg2addnclem2  38781  dvasin  38813  ssnel  46263  icccncfext  47100  dirkercncflem1  47316  fourierdlem81  47400  fourierdlem97  47416  prsal  47531  volico2  47854  indprmfz  48918