![]() |
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 936 nfimd 1993 sbi1v 2327 nfald 2351 nfeqf2OLD 2383 cbv2h 2408 exdistrf 2454 euind 3589 reuind 3609 sbcimdv 3695 cores 5857 tz7.7 5967 tz7.49 7779 omsmolem 7973 php 8386 hta 9010 carddom2 9089 infdif 9319 isf32lem3 9465 alephval2 9682 cfpwsdom 9694 nqerf 10040 zeo 11753 o1rlimmul 14690 catideu 16650 catpropd 16683 ufileu 22051 iscau2 23403 scvxcvx 25064 issgon 30702 cvmsss2 31773 onsucconni 32944 onsucsuccmpi 32950 bj-ssbft 33148 bj-ax12v3ALT 33182 bj-cbv2hv 33235 bj-sbsb 33319 lpolsatN 37509 lpolpolsatN 37510 frege70 39009 sspwtrALT 39818 snlindsntor 43059 0setrec 43249 |
Copyright terms: Public domain | W3C validator |