![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylsyld | Structured version Visualization version GIF version |
Description: A double syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.) |
Ref | Expression |
---|---|
sylsyld.1 | ⊢ (𝜑 → 𝜓) |
sylsyld.2 | ⊢ (𝜑 → (𝜒 → 𝜃)) |
sylsyld.3 | ⊢ (𝜓 → (𝜃 → 𝜏)) |
Ref | Expression |
---|---|
sylsyld | ⊢ (𝜑 → (𝜒 → 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylsyld.2 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) | |
2 | sylsyld.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | sylsyld.3 | . . 3 ⊢ (𝜓 → (𝜃 → 𝜏)) | |
4 | 2, 3 | syl 17 | . 2 ⊢ (𝜑 → (𝜃 → 𝜏)) |
5 | 1, 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: mpsylsyld 69 syl6an 683 axc16gALT 2493 rspc2vd 3911 trintss 5246 onfununi 8292 smoiun 8312 findcard2 9115 findcard2OLD 9235 findcard3 9236 findcard3OLD 9237 inficl 9368 en3lplem2 9556 infxpenlem 9956 alephordi 10017 cardaleph 10032 pwsdompw 10147 cfslb2n 10211 isf32lem10 10305 axdc4lem 10398 zorn2lem2 10440 alephreg 10525 inar1 10718 tskuni 10726 grudomon 10760 nqereu 10872 leltletr 11253 ltleletr 11255 elfz0ubfz0 13552 ssnn0fi 13897 caubnd 15250 sqreulem 15251 bezoutlem1 16427 rppwr 16447 pcprendvds 16719 prmreclem3 16797 ptcmpfi 23180 ufilen 23297 fcfnei 23402 bcthlem5 24708 aaliou 25714 wlkres 28660 wlkiswwlks2 28862 3cyclfrgrrn1 29271 n4cyclfrgr 29277 occon2 30272 occon3 30281 atexch 31365 sigaclci 32771 fisshasheq 33745 pfxwlk 33757 cusgr3cyclex 33770 idinside 34698 exrecfnlem 35879 poimirlem32 36139 heibor1lem 36297 axc16g-o 37425 axc11-o 37442 aomclem2 41411 frege124d 42107 tratrb 42892 trsspwALT2 43175 |
Copyright terms: Public domain | W3C validator |