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 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 487 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏) |
4 | 3 | 3impa 1251 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: opelopabt 4912 ordelinel 5742 ordelinelOLD 5743 nelrnfvne 6261 omass 7547 nnmass 7591 f1imaeng 7902 genpass 9710 adddir 9910 le2tri3i 10046 addsub12 10173 subdir 10343 ltaddsub 10381 leaddsub 10383 div12 10586 xmulass 11989 fldiv2 12522 modsubdir 12601 digit2 12859 muldivbinom2 12909 ccatass 13224 ccatw2s1len 13254 repswcshw 13409 s3tpop 13504 absdiflt 13905 absdifle 13906 binomrisefac 14612 cos01gt0 14760 rpnnen2lem4 14785 rpnnen2lem7 14788 sadass 15031 lubub 16942 lubl 16943 reslmhm2b 18875 ipcl 19797 ma1repveval 20196 mp2pm2mplem5 20434 opnneiss 20732 llyi 21087 nllyi 21088 cfiluweak 21909 cniccibl 23413 ply1term 23764 explog 24144 logrec 24301 4cycl2vnunb 26544 numclwwlkovf2ex 26613 numclwwlk7 26641 lnocoi 26996 hvaddsubass 27282 hvmulcan2 27314 hhssabloilem 27502 hhssnv 27505 homco1 28044 homulass 28045 hoadddir 28047 hoaddsubass 28058 hosubsub4 28061 kbmul 28198 lnopmulsubi 28219 mdsl3 28559 cdj3lem2 28678 probmeasb 29819 signswmnd 29960 bnj563 30067 fnessex 31511 cnicciblnc 32651 incsequz2 32715 ltrncnvatb 34442 jm2.17a 36545 lnrfgtr 36709 ccatw2s1cl 40243 usgredgop 40400 usgr2v1e2w 40478 cusgrsizeinds 40668 4cycl2vnunb-av 41460 frrusgrord0 41503 av-numclwwlkovf2ex 41517 av-numclwwlk7 41545 dignnld 42195 |
Copyright terms: Public domain | W3C validator |