![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > stoic4a | Structured version Visualization version GIF version |
Description: Stoic logic Thema 4
version a. Statement T4 of [Bobzien] p. 117
shows a
reconstructed version of Stoic logic Thema 4: "When from two
assertibles a third follows, and from the third and one (or both) of the
two and one (or more) external assertible(s) another follows, then this
other follows from the first two and the external(s)."
We use 𝜃 to represent the "external" assertibles. This is version a, which is without the phrase "or both"; see stoic4b 1877 for the version with the phrase "or both". (Contributed by David A. Wheeler, 17-Feb-2019.) |
Ref | Expression |
---|---|
stoic4a.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
stoic4a.2 | ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
stoic4a | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | stoic4a.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | 3adant3 1166 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) |
3 | simp1 1170 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜑) | |
4 | simp3 1172 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜃) | |
5 | stoic4a.2 | . 2 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) → 𝜏) | |
6 | 2, 3, 4, 5 | syl3anc 1494 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1111 |
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 199 df-an 387 df-3an 1113 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |