![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > unssad | Structured version Visualization version Unicode version |
Description: If ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
unssad.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
unssad |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unssad.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | unss 3619 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylibr 217 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | simpld 465 |
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-or 376 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-un 3420 df-in 3422 df-ss 3429 |
This theorem is referenced by: ersym 7400 findcard2d 7838 finsschain 7906 r0weon 8468 ackbij1lem16 8690 wunex2 9188 sumsplit 13877 fsumabs 13909 fsumiun 13929 mrieqvlemd 15583 yonedalem1 16205 yonedalem21 16206 yonedalem22 16211 yonffthlem 16215 lsmsp 18357 mplcoe1 18737 mdetunilem9 19693 ordtbas 20256 isufil2 20971 ufileu 20982 filufint 20983 fmfnfm 21021 flimclslem 21047 fclsfnflim 21090 flimfnfcls 21091 imasdsf1olem 21436 mbfeqalem 22646 limcdif 22879 jensenlem1 23960 jensenlem2 23961 jensen 23962 gsumvsca1 28593 gsumvsca2 28594 ordtconlem1 28778 ssmcls 30253 mclsppslem 30269 rngunsnply 36083 mptrcllem 36264 clcnvlem 36274 brtrclfv2 36363 dvnprodlem1 37858 |
Copyright terms: Public domain | W3C validator |