![]() |
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 8485 nnaordi 8557 fineqvlem 9164 dif1ennnALT 9179 xpfiOLD 9220 rankr1ag 9696 cfslb2n 10162 fin23lem27 10222 gchpwdom 10564 prlem934 10927 axpre-sup 11063 cju 12107 xrub 13185 facavg 14155 mulcn2 15438 o1rlimmul 15461 coprm 16547 rpexp 16558 vdwnnlem3 16829 gexdvds 19325 cnpnei 22567 comppfsc 22835 alexsubALTlem3 23352 alexsubALTlem4 23353 iccntr 24136 cfil3i 24585 bcth3 24647 lgseisenlem2 26676 cusgredg 28201 uspgr2wlkeq 28423 ubthlem1 29641 staddi 31017 stadd3i 31019 addltmulALT 31217 cnre2csqlem 32303 tpr2rico 32305 satffunlem2lem1 33810 mclsax 33975 dfrdg4 34474 segconeq 34533 nn0prpwlem 34732 bj-bary1lem1 35720 poimirlem29 36045 fdc 36142 bfplem2 36220 atexchcvrN 37841 dalem3 38065 cdleme3h 38636 cdleme21ct 38730 oexpreposd 40716 cantnfresb 41565 omabs2 41572 sbgoldbwt 45870 sbgoldbst 45871 nnsum4primesodd 45889 nnsum4primesoddALTV 45890 dignn0flhalflem1 46602 |
Copyright terms: Public domain | W3C validator |