![]() |
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 862 pm5.11dc 909 ax16i 1858 mor 2068 ceqsalg 2765 cgsexg 2772 cgsex2g 2773 cgsex4g 2774 spc2egv 2827 spc2gv 2828 spc3egv 2829 spc3gv 2830 disjne 3476 uneqdifeqim 3508 eqifdc 3569 triun 4114 sucssel 4424 ordsucg 4501 regexmidlem1 4532 relresfld 5158 relcoi1 5160 focdmex 6115 f1dmex 6116 dom2d 6772 findcard 6887 nneo 9354 zeo2 9357 uznfz 10100 difelfzle 10131 ssfzo12 10221 facndiv 10714 fisumcom2 11441 fprodssdc 11593 fprodcom2fi 11629 ndvdssub 11929 bezoutlembi 12000 eucalglt 12051 prmind2 12114 coprm 12138 prmdiveq 12230 mhmlin 12812 issubg2m 13002 nsgbi 13017 issubrg2 13322 inopn 13394 basis1 13438 tgss 13456 tgcl 13457 xmeteq0 13752 blssexps 13822 blssex 13823 mopni3 13877 neibl 13884 metss 13887 metcnp3 13904 logbgcd1irr 14278 bj-indsuc 14562 bj-nntrans 14585 |
Copyright terms: Public domain | W3C validator |