| 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 863 pm5.11dc 910 ax16i 1880 mor 2095 ceqsalg 2799 cgsexg 2806 cgsex2g 2807 cgsex4g 2808 spc2egv 2862 spc2gv 2863 spc3egv 2864 spc3gv 2865 disjne 3513 uneqdifeqim 3545 eqifdc 3606 triun 4154 sucssel 4470 ordsucg 4549 regexmidlem1 4580 relresfld 5211 relcoi1 5213 focdmex 6199 f1dmex 6200 dom2d 6863 findcard 6984 nneo 9475 zeo2 9478 uznfz 10224 difelfzle 10255 ssfzo12 10351 facndiv 10882 fisumcom2 11720 fprodssdc 11872 fprodcom2fi 11908 ndvdssub 12212 bezoutlembi 12297 eucalglt 12350 prmind2 12413 coprm 12437 prmdiveq 12529 mhmlin 13270 issubg2m 13496 nsgbi 13511 issubrng2 13943 issubrg2 13974 lmodlema 14025 rmodislmodlem 14083 rmodislmod 14084 lspsnel6 14141 inopn 14446 basis1 14490 tgss 14506 tgcl 14507 xmeteq0 14802 blssexps 14872 blssex 14873 mopni3 14927 neibl 14934 metss 14937 metcnp3 14954 logbgcd1irr 15410 gausslemma2dlem0i 15505 2lgsoddprmlem3 15559 bj-indsuc 15826 bj-nntrans 15849 |
| Copyright terms: Public domain | W3C validator |