Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl3c | Unicode version |
Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 7-Jul-2011.) |
Ref | Expression |
---|---|
syl3c.1 | |
syl3c.2 | |
syl3c.3 | |
syl3c.4 |
Ref | Expression |
---|---|
syl3c |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3c.3 | . 2 | |
2 | syl3c.1 | . . 3 | |
3 | syl3c.2 | . . 3 | |
4 | syl3c.4 | . . 3 | |
5 | 2, 3, 4 | sylc 62 | . 2 |
6 | 1, 5 | mpd 13 | 1 |
Colors of variables: wff set 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: bilukdc 1385 disjiun 3972 tfrlem1 6268 tfrcl 6324 mkvprop 7114 ccfunen 7197 caucvgprprlemval 7621 suplocsrlem 7741 peano5uzti 9291 zfz1iso 10744 lcmneg 11995 prmind2 12041 pcfac 12269 cnmpt12 12854 cnmpt22 12861 limccnp2lem 13212 sbthom 13766 |
Copyright terms: Public domain | W3C validator |