![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqssd | Unicode version |
Description: Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.) |
Ref | Expression |
---|---|
eqssd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
eqssd.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eqssd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqssd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eqssd.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | eqss 3185 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | sylanbrc 417 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-11 1517 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-in 3150 df-ss 3157 |
This theorem is referenced by: eqrd 3188 eqelssd 3189 unissel 3853 intmin 3879 int0el 3889 pwntru 4217 exmidundif 4224 exmidundifim 4225 dmcosseq 4916 relfld 5175 imadif 5315 imain 5317 fimacnv 5666 fo2ndf 6253 tposeq 6273 tfrlemibfn 6354 tfrlemi14d 6359 tfr1onlembfn 6370 tfri1dALT 6377 tfrcllembfn 6383 dcdifsnid 6530 fisbth 6912 en2eqpr 6936 exmidpw 6937 exmidpweq 6938 undifdcss 6952 nnnninfeq2 7158 en2other2 7226 exmidontriimlem3 7253 addnqpr 7591 mulnqpr 7607 distrprg 7618 ltexpri 7643 addcanprg 7646 recexprlemex 7667 aptipr 7671 cauappcvgprlemladd 7688 fzopth 10093 fzosplit 10209 fzouzsplit 10211 frecuzrdgtcl 10445 frecuzrdgdomlem 10450 zsupssdc 11990 phimullem 12260 structcnvcnv 12531 imasaddfnlemg 12794 trivsubgd 13156 trivsubgsnd 13157 trivnsgd 13173 kerf1ghm 13230 conjnmz 13235 lspun 13735 lspsn 13749 lspsnneg 13753 lsp0 13756 lsslsp 13762 mulgrhm2 13925 eltg4i 14032 unitg 14039 tgtop 14045 tgidm 14051 basgen 14057 2basgeng 14059 epttop 14067 ntrin 14101 isopn3 14102 neiuni 14138 tgrest 14146 resttopon 14148 rest0 14156 txdis 14254 hmeontr 14290 xmettx 14487 findset 15175 pwtrufal 15226 pwf1oexmid 15228 |
Copyright terms: Public domain | W3C validator |