![]() |
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 684 axc16gALT 2493 rspc2vd 3959 trintss 5284 onfununi 8380 smoiun 8400 findcard2 9203 findcard3 9316 findcard3OLD 9317 inficl 9463 en3lplem2 9651 infxpenlem 10051 alephordi 10112 cardaleph 10127 pwsdompw 10241 cfslb2n 10306 isf32lem10 10400 axdc4lem 10493 zorn2lem2 10535 alephreg 10620 inar1 10813 tskuni 10821 grudomon 10855 nqereu 10967 leltletr 11350 ltleletr 11352 elfz0ubfz0 13669 ssnn0fi 14023 caubnd 15394 sqreulem 15395 bezoutlem1 16573 rppwr 16594 pcprendvds 16874 prmreclem3 16952 ptcmpfi 23837 ufilen 23954 fcfnei 24059 bcthlem5 25376 aaliou 26395 wlkres 29703 wlkiswwlks2 29905 3cyclfrgrrn1 30314 n4cyclfrgr 30320 occon2 31317 occon3 31326 atexch 32410 dfufd2lem 33557 sigaclci 34113 fisshasheq 35099 pfxwlk 35108 cusgr3cyclex 35121 idinside 36066 exrecfnlem 37362 poimirlem32 37639 heibor1lem 37796 axc16g-o 38916 axc11-o 38933 aomclem2 43044 frege124d 43751 tratrb 44534 trsspwALT2 44817 |
Copyright terms: Public domain | W3C validator |