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 1688 and stoic1b 1689 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 449 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
3 | 2 | con3dimp 456 | 1 ⊢ ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: stoic1b 1689 posn 5110 frsn 5112 relimasn 5407 nssdmovg 6714 iblss 23377 midexlem 25387 colhp 25462 xaddeq0 28907 xrge0npcan 29025 unccur 32562 lindsenlbs 32574 itg2addnclem2 32632 dvasin 32666 ssnel 38227 icccncfext 38773 dirkercncflem1 38996 fourierdlem81 39080 fourierdlem97 39096 volico2 39531 |
Copyright terms: Public domain | W3C validator |