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 905 nfimd 1886 sbi1vOLD 2314 nfald 2338 cbv2w 2348 cbv2 2414 cbv2h 2417 exdistrf 2461 mo4 2643 vtoclgft 3551 euind 3712 reuind 3741 sbcimdv 3840 cores 6095 tz7.7 6210 oprabidw 7176 tz7.49 8070 omsmolem 8269 php 8689 hta 9314 carddom2 9394 infdif 9619 isf32lem3 9765 alephval2 9982 cfpwsdom 9994 nqerf 10340 zeo 12056 o1rlimmul 14963 catideu 16934 catpropd 16967 ufileu 22455 iscau2 23807 scvxcvx 25490 issgon 31281 cvmsss2 32418 satffunlem2lem1 32548 onsucconni 33682 onsucsuccmpi 33688 bj-peircestab 33785 bj-cbvalimt 33869 bj-cbveximt 33870 bj-ax12v3ALT 33917 bj-wnf2 33949 bj-cbv2hv 34016 bj-sbsb 34057 bj-nfald 34321 lpolsatN 38504 lpolpolsatN 38505 frege70 40157 sspwtrALT 41033 snlindsntor 44454 0setrec 44734 |
Copyright terms: Public domain | W3C validator |