Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mulid2i | Structured version Visualization version GIF version |
Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
Ref | Expression |
---|---|
axi.1 | ⊢ 𝐴 ∈ ℂ |
Ref | Expression |
---|---|
mulid2i | ⊢ (1 · 𝐴) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axi.1 | . 2 ⊢ 𝐴 ∈ ℂ | |
2 | mulid2 10628 | . 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (1 · 𝐴) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ∈ wcel 2105 (class class class)co 7145 ℂcc 10523 1c1 10526 · cmul 10530 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-resscn 10582 ax-1cn 10583 ax-icn 10584 ax-addcl 10585 ax-mulcl 10587 ax-mulcom 10589 ax-mulass 10591 ax-distr 10592 ax-1rid 10595 ax-cnre 10598 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-iota 6307 df-fv 6356 df-ov 7148 |
This theorem is referenced by: 00id 10803 halfpm6th 11846 div4p1lem1div2 11880 3halfnz 12049 crreczi 13577 fac2 13627 hashxplem 13782 bpoly1 15393 bpoly2 15399 bpoly3 15400 bpoly4 15401 efival 15493 ef01bndlem 15525 3dvdsdec 15669 3dvds2dec 15670 odd2np1lem 15677 m1expo 15714 m1exp1 15715 nno 15721 divalglem5 15736 gcdaddmlem 15860 prmo2 16364 dec5nprm 16390 2exp8 16411 13prm 16437 23prm 16440 37prm 16442 43prm 16443 83prm 16444 139prm 16445 163prm 16446 317prm 16447 631prm 16448 1259lem2 16453 1259lem3 16454 1259lem4 16455 1259lem5 16456 2503lem1 16458 2503lem2 16459 2503lem3 16460 2503prm 16461 4001lem1 16462 4001lem2 16463 4001lem3 16464 4001lem4 16465 cnmsgnsubg 20649 sin2pim 24998 cos2pim 24999 sincosq3sgn 25013 sincosq4sgn 25014 tangtx 25018 sincosq1eq 25025 sincos4thpi 25026 sincos6thpi 25028 pige3ALT 25032 abssinper 25033 ang180lem2 25315 ang180lem3 25316 1cubr 25347 asin1 25399 dvatan 25440 log2cnv 25449 log2ublem3 25453 log2ub 25454 logfacbnd3 25726 bclbnd 25783 bpos1 25786 bposlem8 25794 lgsdilem 25827 lgsdir2lem1 25828 lgsdir2lem4 25831 lgsdir2lem5 25832 lgsdir2 25833 lgsdir 25835 2lgsoddprmlem3c 25915 dchrisum0flblem1 26011 rpvmasum2 26015 log2sumbnd 26047 ax5seglem7 26648 ex-fl 28153 ipasslem10 28543 hisubcomi 28808 normlem1 28814 normlem9 28822 norm-ii-i 28841 normsubi 28845 polid2i 28861 lnophmlem2 29721 lnfn0i 29746 nmopcoi 29799 unierri 29808 addltmulALT 30150 dpmul4 30517 sgnmul 31699 logdivsqrle 31820 hgt750lem 31821 hgt750lem2 31822 problem4 32808 quad3 32810 cnndvlem1 33773 sin2h 34763 poimirlem26 34799 cntotbnd 34955 sqdeccom12 39053 ex-decpmul 39056 areaquad 39701 coskpi2 42023 stoweidlem13 42175 wallispilem2 42228 wallispilem4 42230 wallispi2lem1 42233 dirkerper 42258 dirkertrigeqlem1 42260 dirkercncflem1 42265 sqwvfoura 42390 sqwvfourb 42391 fourierswlem 42392 fouriersw 42393 257prm 43600 fmtnofac1 43609 fmtno4prmfac 43611 fmtno4nprmfac193 43613 fmtno5faclem1 43618 fmtno5faclem2 43619 139prmALT 43636 127prm 43640 11t31e341 43774 2exp340mod341 43775 nfermltl8rev 43784 tgoldbach 43859 |
Copyright terms: Public domain | W3C validator |