![]() |
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 911 nfimd 1898 nfald 2322 cbv2w 2334 cbv2 2402 cbv2h 2405 exdistrf 2446 mo4 2561 euind 3686 reuind 3715 sbcimdv 3817 sbcimdvOLD 3818 cores 6205 tz7.7 6347 oprabidw 7392 tz7.49 8395 omsmolem 8607 phpOLD 9172 hta 9841 carddom2 9921 infdif 10153 isf32lem3 10299 alephval2 10516 cfpwsdom 10528 nqerf 10874 zeo 12597 o1rlimmul 15510 catideu 17563 catpropd 17597 ufileu 23293 iscau2 24664 scvxcvx 26358 issgon 32786 cvmsss2 33932 satffunlem2lem1 34062 onsucconni 34962 onsucsuccmpi 34968 bj-peircestab 35069 bj-cbvalimt 35156 bj-cbveximt 35157 bj-ax12v3ALT 35204 bj-wnf2 35236 bj-cbv2hv 35315 bj-sbsb 35355 bj-nfald 35658 lpolsatN 40001 lpolpolsatN 40002 naddcnffo 41727 frege70 42297 sspwtrALT 43196 snlindsntor 46642 0setrec 47239 |
Copyright terms: Public domain | W3C validator |