| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > syl56 | Structured version Visualization version GIF version | ||
| Description: Combine syl5 34 and syl6 35. (Contributed by NM, 14-Nov-2013.) |
| Ref | Expression |
|---|---|
| syl56.1 | ⊢ (𝜑 → 𝜓) |
| syl56.2 | ⊢ (𝜒 → (𝜓 → 𝜃)) |
| syl56.3 | ⊢ (𝜃 → 𝜏) |
| Ref | Expression |
|---|---|
| syl56 | ⊢ (𝜒 → (𝜑 → 𝜏)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syl56.1 | . 2 ⊢ (𝜑 → 𝜓) | |
| 2 | syl56.2 | . . 3 ⊢ (𝜒 → (𝜓 → 𝜃)) | |
| 3 | syl56.3 | . . 3 ⊢ (𝜃 → 𝜏) | |
| 4 | 2, 3 | syl6 35 | . 2 ⊢ (𝜒 → (𝜓 → 𝜏)) |
| 5 | 1, 4 | syl5 34 | 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: orim12dALT 912 nfimd 1894 nfald 2328 cbv2w 2339 cbv2 2408 cbv2h 2411 exdistrf 2452 mo4 2566 euind 3730 reuind 3759 sbcimdv 3859 cores 6269 tz7.7 6410 oprabidw 7462 tz7.49 8485 omsmolem 8695 phpOLD 9259 hta 9937 carddom2 10017 infdif 10248 isf32lem3 10395 alephval2 10612 cfpwsdom 10624 nqerf 10970 zeo 12704 o1rlimmul 15655 catideu 17718 catpropd 17752 ufileu 23927 iscau2 25311 scvxcvx 27029 issgon 34124 cbvex1v 35088 cvmsss2 35279 satffunlem2lem1 35409 onsucconni 36438 onsucsuccmpi 36444 bj-peircestab 36554 bj-cbvalimt 36640 bj-cbveximt 36641 bj-ax12v3ALT 36687 bj-wnf2 36719 bj-cbv2hv 36798 bj-sbsb 36838 bj-nfald 37138 lpolsatN 41490 lpolpolsatN 41491 naddcnffo 43377 frege70 43946 sspwtrALT 44842 snlindsntor 48388 0setrec 49223 |
| Copyright terms: Public domain | W3C validator |