![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl5com | Unicode version |
Description: Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.) |
Ref | Expression |
---|---|
syl5com.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl5com.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl5com |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5com.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1d 22 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | syl5com.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sylcom 25 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: com12 27 syl5 28 pm2.6dc 759 pm5.11dc 815 ax16i 1738 mor 1942 ceqsalg 2582 cgsexg 2589 cgsex2g 2590 cgsex4g 2591 spc2egv 2642 spc2gv 2643 spc3egv 2644 spc3gv 2645 disjne 3273 uneqdifeqim 3308 triun 3867 sucssel 4161 ordsucg 4228 regexmidlem1 4258 relresfld 4847 relcoi1 4849 fornex 5742 f1dmex 5743 rdgon 5973 dom2d 6253 findcard 6345 nneo 8341 zeo2 8344 uznfz 8965 difelfzle 8992 ssfzo12 9080 bj-indsuc 10052 bj-nntrans 10076 |
Copyright terms: Public domain | W3C validator |