New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > sylc | Unicode version |
Description: A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.) |
Ref | Expression |
---|---|
sylc.1 | |
sylc.2 | |
sylc.3 |
Ref | Expression |
---|---|
sylc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylc.1 | . . 3 | |
2 | sylc.2 | . . 3 | |
3 | sylc.3 | . . 3 | |
4 | 1, 2, 3 | syl2im 34 | . 2 |
5 | 4 | pm2.43i 43 | 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: syl3c 57 mpsyl 59 jc 139 2thd 231 jca 518 syl2anc 642 nfimd 1808 ax12 1935 ax12from12o 2156 equid1 2158 elex22 2870 elex2 2871 spcimdv 2936 spsbcd 3059 nnceleq 4430 tfinltfin 4501 sfinltfin 4535 sfin111 4536 phialllem1 4616 fvopab4t 5385 fvelrn 5413 frd 5922 refd 5927 enadjlem1 6059 enadj 6060 enprmaplem3 6078 1cnc 6139 |
Copyright terms: Public domain | W3C validator |