![]() |
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: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: bilukdc 1375 disjiun 3932 tfrlem1 6213 tfrcl 6269 mkvprop 7040 ccfunen 7096 caucvgprprlemval 7520 suplocsrlem 7640 peano5uzti 9183 zfz1iso 10616 lcmneg 11791 prmind2 11837 cnmpt12 12495 cnmpt22 12502 limccnp2lem 12853 sbthom 13396 |
Copyright terms: Public domain | W3C validator |