| 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 1772 and stoic1b 1773 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 1773 posn 5771 frsn 5773 relimasn 6103 nssdmovg 7615 iblss 25840 midexlem 28700 colhp 28778 clwwlknon0 30112 xaddeq0 32757 xrge0npcan 33025 elrgspnsubrunlem2 33252 madjusmdetlem2 33827 unccur 37610 lindsenlbs 37622 itg2addnclem2 37679 dvasin 37711 ssnel 45048 icccncfext 45902 dirkercncflem1 46118 fourierdlem81 46202 fourierdlem97 46218 prsal 46333 volico2 46656 |
| Copyright terms: Public domain | W3C validator |