|   | 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 2495 rspc2vd 3947 trintss 5278 onfununi 8381 smoiun 8401 findcard2 9204 findcard3 9318 findcard3OLD 9319 inficl 9465 en3lplem2 9653 infxpenlem 10053 alephordi 10114 cardaleph 10129 pwsdompw 10243 cfslb2n 10308 isf32lem10 10402 axdc4lem 10495 zorn2lem2 10537 alephreg 10622 inar1 10815 tskuni 10823 grudomon 10857 nqereu 10969 leltletr 11352 ltleletr 11354 elfz0ubfz0 13672 ssnn0fi 14026 caubnd 15397 sqreulem 15398 bezoutlem1 16576 rppwr 16597 pcprendvds 16878 prmreclem3 16956 ptcmpfi 23821 ufilen 23938 fcfnei 24043 bcthlem5 25362 aaliou 26380 wlkres 29688 wlkiswwlks2 29895 3cyclfrgrrn1 30304 n4cyclfrgr 30310 occon2 31307 occon3 31316 atexch 32400 dfufd2lem 33577 sigaclci 34133 fisshasheq 35120 pfxwlk 35129 cusgr3cyclex 35141 idinside 36085 exrecfnlem 37380 poimirlem32 37659 heibor1lem 37816 axc16g-o 38935 axc11-o 38952 aomclem2 43067 frege124d 43774 tratrb 44556 trsspwALT2 44839 | 
| Copyright terms: Public domain | W3C validator |