| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3syld | Structured version Visualization version GIF version | ||
| Description: Triple syllogism deduction. Deduction associated with 3syld 60. (Contributed by Jeff Hankins, 4-Aug-2009.) |
| Ref | Expression |
|---|---|
| 3syld.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| 3syld.2 | ⊢ (𝜑 → (𝜒 → 𝜃)) |
| 3syld.3 | ⊢ (𝜑 → (𝜃 → 𝜏)) |
| Ref | Expression |
|---|---|
| 3syld | ⊢ (𝜑 → (𝜓 → 𝜏)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3syld.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | 3syld.2 | . . 3 ⊢ (𝜑 → (𝜒 → 𝜃)) | |
| 3 | 1, 2 | syld 47 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
| 4 | 3syld.3 | . 2 ⊢ (𝜑 → (𝜃 → 𝜏)) | |
| 5 | 3, 4 | syld 47 | 1 ⊢ (𝜑 → (𝜓 → 𝜏)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
| This theorem is referenced by: oaordi 8584 nnaordi 8656 fineqvlem 9298 dif1ennnALT 9311 xpfiOLD 9359 rankr1ag 9842 cfslb2n 10308 fin23lem27 10368 gchpwdom 10710 prlem934 11073 axpre-sup 11209 cju 12262 xrub 13354 facavg 14340 mulcn2 15632 o1rlimmul 15655 coprm 16748 rpexp 16759 vdwnnlem3 17035 gexdvds 19602 cnpnei 23272 comppfsc 23540 alexsubALTlem3 24057 alexsubALTlem4 24058 iccntr 24843 cfil3i 25303 bcth3 25365 lgseisenlem2 27420 cusgredg 29441 uspgr2wlkeq 29664 ubthlem1 30889 staddi 32265 stadd3i 32267 addltmulALT 32465 expgt0b 32818 cnre2csqlem 33909 tpr2rico 33911 satffunlem2lem1 35409 mclsax 35574 dfrdg4 35952 segconeq 36011 nn0prpwlem 36323 bj-bary1lem1 37312 poimirlem29 37656 fdc 37752 bfplem2 37830 atexchcvrN 39442 dalem3 39666 cdleme3h 40237 cdleme21ct 40331 oexpreposd 42357 cantnfresb 43337 omabs2 43345 naddwordnexlem4 43414 sbgoldbwt 47764 sbgoldbst 47765 nnsum4primesodd 47783 nnsum4primesoddALTV 47784 dignn0flhalflem1 48536 |
| Copyright terms: Public domain | W3C validator |