Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mulcli | Structured version Visualization version Unicode version |
Description: Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Ref | Expression |
---|---|
axi.1 | |
axi.2 |
Ref | Expression |
---|---|
mulcli |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axi.1 | . 2 | |
2 | axi.2 | . 2 | |
3 | mulcl 10020 | . 2 | |
4 | 1, 2, 3 | mp2an 708 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wcel 1990 (class class class)co 6650 cc 9934 cmul 9941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-mulcl 9998 |
This theorem depends on definitions: df-bi 197 df-an 386 |
This theorem is referenced by: mul02lem2 10213 addid1 10216 cnegex2 10218 ixi 10656 2mulicn 11255 numma 11557 nummac 11558 9t11e99 11671 9t11e99OLD 11672 decbin2 11683 irec 12964 binom2i 12974 crreczi 12989 3dec 13050 sq10OLD 13051 3decOLD 13053 nn0opthi 13057 faclbnd4lem1 13080 rei 13896 imi 13897 iseraltlem2 14413 bpoly3 14789 bpoly4 14790 3dvdsdec 15054 3dvdsdecOLD 15055 3dvds2dec 15056 3dvds2decOLD 15057 odd2np1 15065 gcdaddmlem 15245 3lcm2e6woprm 15328 6lcm4e12 15329 modxai 15772 mod2xnegi 15775 decexp2 15779 decsplitOLD 15791 karatsuba 15792 karatsubaOLD 15793 sinhalfpilem 24215 ef2pi 24229 ef2kpi 24230 efper 24231 sinperlem 24232 sin2kpi 24235 cos2kpi 24236 sin2pim 24237 cos2pim 24238 sincos4thpi 24265 sincos6thpi 24267 pige3 24269 abssinper 24270 efeq1 24275 logneg 24334 logm1 24335 eflogeq 24348 logimul 24360 logneg2 24361 cxpsqrt 24449 root1eq1 24496 cxpeq 24498 ang180lem1 24539 ang180lem3 24541 ang180lem4 24542 1cubrlem 24568 1cubr 24569 quart1lem 24582 asin1 24621 atanlogsublem 24642 log2ublem2 24674 log2ublem3 24675 log2ub 24676 bclbnd 25005 bposlem8 25016 bposlem9 25017 lgsdir2lem5 25054 2lgsoddprmlem3c 25137 2lgsoddprmlem3d 25138 ax5seglem7 25815 ip0i 27680 ip1ilem 27681 ipasslem10 27694 siilem1 27706 normlem0 27966 normlem1 27967 normlem2 27968 normlem3 27969 normlem5 27971 normlem7 27973 bcseqi 27977 norm-ii-i 27994 normpar2i 28013 polid2i 28014 h1de2i 28412 lnopunilem1 28869 lnophmlem2 28876 dfdec100 29576 dpmul100 29605 dp3mul10 29606 dpmul1000 29607 dpexpp1 29616 dpmul 29621 dpmul4 29622 ballotth 30599 efmul2picn 30674 itgexpif 30684 vtscl 30716 circlemeth 30718 hgt750lem 30729 problem2 31559 problem2OLD 31560 problem4 31562 quad3 31564 logi 31620 heiborlem6 33615 proot1ex 37779 areaquad 37802 coskpi2 40077 cosnegpi 40078 cosknegpi 40080 wallispilem4 40285 dirkerper 40313 dirkertrigeq 40318 dirkercncflem2 40321 fourierdlem57 40380 fourierdlem62 40385 fourierswlem 40447 fmtnorec3 41460 fmtnorec4 41461 lighneallem3 41524 3exp4mod41 41533 41prothprmlem1 41534 zlmodzxzequap 42288 nn0sumshdiglemB 42414 i2linesi 42524 |
Copyright terms: Public domain | W3C validator |