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 1703 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 1081 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) |
3 | simp1 1061 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜑) | |
4 | simp3 1063 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜃) | |
5 | stoic4a.2 | . 2 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) → 𝜏) | |
6 | 2, 3, 4, 5 | syl3anc 1326 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |