![]() |
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 7798 nnaordi 7870 fineqvlem 8342 dif1en 8361 xpfi 8399 rankr1ag 8841 cfslb2n 9303 fin23lem27 9363 gchpwdom 9705 prlem934 10068 axpre-sup 10203 cju 11229 xrub 12356 facavg 13303 mulcn2 14546 o1rlimmul 14569 coprm 15646 rpexp 15655 vdwnnlem3 15924 gexdvds 18220 cnpnei 21291 comppfsc 21558 alexsubALTlem3 22075 alexsubALTlem4 22076 iccntr 22846 cfil3i 23288 bcth3 23349 lgseisenlem2 25322 cusgredg 26552 uspgr2wlkeq 26774 ubthlem1 28057 staddi 29436 stadd3i 29438 addltmulALT 29636 cnre2csqlem 30287 tpr2rico 30289 mclsax 31795 dfrdg4 32386 segconeq 32445 nn0prpwlem 32645 bj-bary1lem1 33491 poimirlem29 33770 fdc 33873 bfplem2 33954 atexchcvrN 35248 dalem3 35472 cdleme3h 36044 cdleme21ct 36138 sbgoldbwt 42194 sbgoldbst 42195 nnsum4primesodd 42213 nnsum4primesoddALTV 42214 dignn0flhalflem1 42938 |
Copyright terms: Public domain | W3C validator |