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-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: com12 30 syl5 32 pm2.6dc 832 pm5.11dc 879 ax16i 1814 mor 2019 ceqsalg 2688 cgsexg 2695 cgsex2g 2696 cgsex4g 2697 spc2egv 2749 spc2gv 2750 spc3egv 2751 spc3gv 2752 disjne 3386 uneqdifeqim 3418 eqifdc 3476 triun 4009 sucssel 4316 ordsucg 4388 regexmidlem1 4418 relresfld 5038 relcoi1 5040 fornex 5981 f1dmex 5982 dom2d 6635 findcard 6750 nneo 9122 zeo2 9125 uznfz 9851 difelfzle 9879 ssfzo12 9969 facndiv 10453 fisumcom2 11175 ndvdssub 11554 bezoutlembi 11620 eucalglt 11665 prmind2 11728 coprm 11749 inopn 12097 basis1 12141 tgss 12159 tgcl 12160 xmeteq0 12455 blssexps 12525 blssex 12526 mopni3 12580 neibl 12587 metss 12590 metcnp3 12607 bj-indsuc 13053 bj-nntrans 13076 |
Copyright terms: Public domain | W3C validator |