![]() |
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 758 pm5.11dc 814 ax16i 1735 mor 1939 ceqsalg 2576 cgsexg 2583 cgsex2g 2584 cgsex4g 2585 spc2egv 2636 spc2gv 2637 spc3egv 2638 spc3gv 2639 disjne 3267 uneqdifeqim 3302 triun 3858 sucssel 4127 ordsucg 4194 regexmidlem1 4218 relresfld 4790 relcoi1 4792 fornex 5684 f1dmex 5685 rdgon 5913 dom2d 6189 nneo 8117 zeo2 8120 uznfz 8735 difelfzle 8762 ssfzo12 8850 bj-indsuc 9387 bj-nntrans 9411 |
Copyright terms: Public domain | W3C validator |