| 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: |
| 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 864 pm5.11dc 911 ax16i 1881 mor 2096 ceqsalg 2800 cgsexg 2807 cgsex2g 2808 cgsex4g 2809 spc2egv 2863 spc2gv 2864 spc3egv 2865 spc3gv 2866 disjne 3514 uneqdifeqim 3546 eqifdc 3607 triun 4155 sucssel 4471 ordsucg 4550 regexmidlem1 4581 relresfld 5212 relcoi1 5214 focdmex 6200 f1dmex 6201 dom2d 6864 findcard 6985 nneo 9476 zeo2 9479 uznfz 10225 difelfzle 10256 ssfzo12 10353 facndiv 10884 fisumcom2 11749 fprodssdc 11901 fprodcom2fi 11937 ndvdssub 12241 bezoutlembi 12326 eucalglt 12379 prmind2 12442 coprm 12466 prmdiveq 12558 mhmlin 13299 issubg2m 13525 nsgbi 13540 issubrng2 13972 issubrg2 14003 lmodlema 14054 rmodislmodlem 14112 rmodislmod 14113 lspsnel6 14170 inopn 14475 basis1 14519 tgss 14535 tgcl 14536 xmeteq0 14831 blssexps 14901 blssex 14902 mopni3 14956 neibl 14963 metss 14966 metcnp3 14983 logbgcd1irr 15439 gausslemma2dlem0i 15534 2lgsoddprmlem3 15588 bj-indsuc 15864 bj-nntrans 15887 |
| Copyright terms: Public domain | W3C validator |