![]() |
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 axc16gALT 2395 trintss 4802 onfununi 7483 smoiun 7503 findcard2 8241 findcard3 8244 inficl 8372 en3lplem2 8550 r1sdom 8675 infxpenlem 8874 alephordi 8935 cardaleph 8950 pwsdompw 9064 cfslb2n 9128 isf32lem10 9222 axdc4lem 9315 zorn2lem2 9357 alephreg 9442 inar1 9635 tskuni 9643 grudomon 9677 nqereu 9789 ltleletr 10168 elfz0ubfz0 12482 ssnn0fi 12824 caubnd 14142 sqreulem 14143 bezoutlem1 15303 pcprendvds 15592 prmreclem3 15669 ptcmpfi 21664 ufilen 21781 fcfnei 21886 bcthlem5 23171 aaliou 24138 wlkres 26623 wlkiswwlks2 26829 rspc2vd 27245 3cyclfrgrrn1 27265 n4cyclfrgr 27271 occon2 28275 occon3 28284 atexch 29368 sigaclci 30323 frmin 31867 idinside 32316 poimirlem32 33571 heibor1lem 33738 axc16g-o 34538 axc11-o 34555 aomclem2 37942 frege124d 38370 tratrb 39063 trsspwALT2 39363 leltletr 41633 |
Copyright terms: Public domain | W3C validator |