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 28 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: com12 30 syl5 32 pm2.6dc 792 pm5.11dc 848 ax16i 1779 mor 1983 ceqsalg 2627 cgsexg 2634 cgsex2g 2635 cgsex4g 2636 spc2egv 2687 spc2gv 2688 spc3egv 2689 spc3gv 2690 disjne 3297 uneqdifeqim 3328 triun 3888 sucssel 4179 ordsucg 4246 regexmidlem1 4276 relresfld 4867 relcoi1 4869 fornex 5762 f1dmex 5763 rdgon 5996 dom2d 6276 findcard 6372 nneo 8450 zeo2 8453 uznfz 9120 difelfzle 9145 ssfzo12 9233 facndiv 9666 ndvdssub 10330 bezoutlembi 10394 eucalglt 10439 prmind2 10502 coprm 10523 bj-indsuc 10723 bj-nntrans 10746 |
Copyright terms: Public domain | W3C validator |