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 847 pm5.11dc 894 ax16i 1830 mor 2041 ceqsalg 2714 cgsexg 2721 cgsex2g 2722 cgsex4g 2723 spc2egv 2775 spc2gv 2776 spc3egv 2777 spc3gv 2778 disjne 3416 uneqdifeqim 3448 eqifdc 3506 triun 4039 sucssel 4346 ordsucg 4418 regexmidlem1 4448 relresfld 5068 relcoi1 5070 fornex 6013 f1dmex 6014 dom2d 6667 findcard 6782 nneo 9161 zeo2 9164 uznfz 9890 difelfzle 9918 ssfzo12 10008 facndiv 10492 fisumcom2 11214 ndvdssub 11634 bezoutlembi 11700 eucalglt 11745 prmind2 11808 coprm 11829 inopn 12180 basis1 12224 tgss 12242 tgcl 12243 xmeteq0 12538 blssexps 12608 blssex 12609 mopni3 12663 neibl 12670 metss 12673 metcnp3 12690 bj-indsuc 13136 bj-nntrans 13159 |
Copyright terms: Public domain | W3C validator |