| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > stoic3 | Structured version Visualization version GIF version | ||
| Description: Stoic logic Thema 3. Statement T3 of [Bobzien] p. 116-117 discusses Stoic logic Thema 3. "When from two (assemblies) a third follows, and from the one that follows (i.e., the third) together with another, external assumption, another follows, then that other follows from the first two and the externally co-assumed one. (Simp. Cael. 237.2-4)" (Contributed by David A. Wheeler, 17-Feb-2019.) |
| Ref | Expression |
|---|---|
| stoic3.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
| stoic3.2 | ⊢ ((𝜒 ∧ 𝜃) → 𝜏) |
| Ref | Expression |
|---|---|
| stoic3 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | stoic3.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
| 2 | stoic3.2 | . . 3 ⊢ ((𝜒 ∧ 𝜃) → 𝜏) | |
| 3 | 1, 2 | sylan 580 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏) |
| 4 | 3 | 3impa 1110 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 df-3an 1089 |
| This theorem is referenced by: opelopabt 5537 ordelinel 6485 nelrnfvne 7097 omass 8618 nnmass 8662 f1imaeng 9054 ssfi 9213 genpass 11049 adddir 11252 le2tri3i 11391 addsub12 11521 subdir 11697 ltaddsub 11737 leaddsub 11739 div12 11944 xmulass 13329 fldiv2 13901 modsubdir 13981 digit2 14275 muldivbinom2 14302 ccatass 14626 ccatw2s1cl 14662 repswcshw 14850 s3tpop 14948 absdiflt 15356 absdifle 15357 binomrisefac 16078 cos01gt0 16227 rpnnen2lem4 16253 rpnnen2lem7 16256 sadass 16508 lubub 18556 lubl 18557 symggrplem 18897 reslmhm2b 21053 cncrng 21401 ipcl 21651 ma1repveval 22577 mp2pm2mplem5 22816 opnneiss 23126 llyi 23482 nllyi 23483 cfiluweak 24304 cniccibl 25876 cnicciblnc 25878 ply1term 26243 explog 26636 logrec 26806 usgredgop 29187 usgr2v1e2w 29269 cusgrsizeinds 29470 clwwlknonex2 30128 4cycl2vnunb 30309 frrusgrord0lem 30358 frrusgrord0 30359 numclwwlk7 30410 lnocoi 30776 hvaddsubass 31060 hvmulcan2 31092 hhssabloilem 31280 hhssnv 31283 homco1 31820 homulass 31821 hoadddir 31823 hoaddsubass 31834 hosubsub4 31837 kbmul 31974 lnopmulsubi 31995 mdsl3 32335 cdj3lem2 32454 probmeasb 34432 signswmnd 34572 bnj563 34757 revpfxsfxrev 35121 lfuhgr2 35124 fnessex 36347 incsequz2 37756 ltrncnvatb 40140 jm2.17a 42972 lnrfgtr 43132 bdaybndex 43444 limsupvaluz2 45753 prsssprel 47475 dignnld 48524 |
| Copyright terms: Public domain | W3C validator |