Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > stoic4a | 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 1410 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 1002 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) |
3 | simp1 982 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜑) | |
4 | simp3 984 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜃) | |
5 | stoic4a.2 | . 2 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) → 𝜏) | |
6 | 2, 3, 4, 5 | syl3anc 1217 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |