![]() |
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 1775 and stoic1b 1776 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 414 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
3 | 2 | con3dimp 410 | 1 ⊢ ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓) |
Colors of variables: wff setvar class |
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 206 df-an 398 |
This theorem is referenced by: stoic1b 1776 posn 5762 frsn 5764 relimasn 6084 nssdmovg 7589 iblss 25322 midexlem 27974 colhp 28052 clwwlknon0 29377 xaddeq0 31997 xrge0npcan 32226 unccur 36519 lindsenlbs 36531 itg2addnclem2 36588 dvasin 36620 ssnel 43775 icccncfext 44651 dirkercncflem1 44867 fourierdlem81 44951 fourierdlem97 44967 prsal 45082 volico2 45405 |
Copyright terms: Public domain | W3C validator |