![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > stoic1a | Structured version Visualization version GIF version |
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 1768 and stoic1b 1769 to represent each side. (Contributed by David A. Wheeler, 16-Feb-2019.) (Proof shortened by Wolf Lammen, 21-May-2020.) |
Ref | Expression |
---|---|
stoic1.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Ref | Expression |
---|---|
stoic1a | ⊢ ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | stoic1.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) | |
2 | 1 | ex 412 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
3 | 2 | con3dimp 408 | 1 ⊢ ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓) |
Colors of variables: wff setvar class |
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 1769 posn 5773 frsn 5775 relimasn 6104 nssdmovg 7614 iblss 25854 midexlem 28714 colhp 28792 clwwlknon0 30121 xaddeq0 32763 xrge0npcan 33007 madjusmdetlem2 33788 unccur 37589 lindsenlbs 37601 itg2addnclem2 37658 dvasin 37690 ssnel 44980 icccncfext 45842 dirkercncflem1 46058 fourierdlem81 46142 fourierdlem97 46158 prsal 46273 volico2 46596 |
Copyright terms: Public domain | W3C validator |