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 1374 disjiun 3919 tfrlem1 6198 tfrcl 6254 mkvprop 7025 ccfunen 7072 caucvgprprlemval 7489 suplocsrlem 7609 peano5uzti 9152 zfz1iso 10577 lcmneg 11744 prmind2 11790 cnmpt12 12445 cnmpt22 12452 limccnp2lem 12803 sbthom 13210 |
Copyright terms: Public domain | W3C validator |