![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssdifd | Structured version Visualization version Unicode version |
Description: If ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ssdifd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ssdifd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssdifd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ssdif 3579 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-v 3058 df-dif 3418 df-in 3422 df-ss 3429 |
This theorem is referenced by: ssdif2d 3583 domunsncan 7697 fin1a2lem13 8867 seqcoll2 12660 rpnnen2lem11 14325 coprmprod 14726 mrieqv2d 15593 mrissmrid 15595 mreexexlem4d 15601 acsfiindd 16471 lsppratlem3 18420 lsppratlem4 18421 f1lindf 19428 lpss3 20208 lpcls 20428 fin1aufil 20995 rrxmval 22407 rrxmetlem 22409 uniioombllem3 22591 i1fmul 22702 itg1addlem4 22705 itg1climres 22720 limciun 22897 ig1peu 23170 ig1peuOLD 23171 ig1pdvds 23176 ig1pdvdsOLD 23182 nbgrassovt 25211 usgreghash2spotv 25842 sitgclg 29223 mthmpps 30268 poimirlem11 31995 poimirlem12 31996 poimirlem15 31999 dochfln0 35089 lcfl6 35112 lcfrlem16 35170 hdmaprnlem4N 35468 caragendifcl 38372 |
Copyright terms: Public domain | W3C validator |