![]() |
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 10375 | . 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (1 · 𝐴) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1601 ∈ wcel 2106 (class class class)co 6922 ℂcc 10270 1c1 10273 · cmul 10277 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-9 2115 ax-10 2134 ax-11 2149 ax-12 2162 ax-13 2333 ax-ext 2753 ax-resscn 10329 ax-1cn 10330 ax-icn 10331 ax-addcl 10332 ax-mulcl 10334 ax-mulcom 10336 ax-mulass 10338 ax-distr 10339 ax-1rid 10342 ax-cnre 10345 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2763 df-cleq 2769 df-clel 2773 df-nfc 2920 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3399 df-dif 3794 df-un 3796 df-in 3798 df-ss 3805 df-nul 4141 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4672 df-br 4887 df-iota 6099 df-fv 6143 df-ov 6925 |
This theorem is referenced by: 00id 10551 halfpm6th 11603 div4p1lem1div2 11637 3halfnz 11808 crreczi 13308 fac2 13384 hashxplem 13534 bpoly1 15184 bpoly2 15190 bpoly3 15191 bpoly4 15192 efival 15284 ef01bndlem 15316 3dvdsdec 15460 3dvds2dec 15461 odd2np1lem 15468 m1expo 15505 m1exp1 15506 nno 15512 divalglem5 15527 gcdaddmlem 15651 prmo2 16148 dec5nprm 16174 2exp8 16195 13prm 16221 23prm 16224 37prm 16226 43prm 16227 83prm 16228 139prm 16229 163prm 16230 317prm 16231 631prm 16232 1259lem2 16237 1259lem3 16238 1259lem4 16239 1259lem5 16240 2503lem1 16242 2503lem2 16243 2503lem3 16244 2503prm 16245 4001lem1 16246 4001lem2 16247 4001lem3 16248 4001lem4 16249 cnmsgnsubg 20318 sin2pim 24675 cos2pim 24676 sincosq3sgn 24690 sincosq4sgn 24691 tangtx 24695 sincosq1eq 24702 sincos4thpi 24703 sincos6thpi 24705 pige3 24707 abssinper 24708 ang180lem2 24988 ang180lem3 24989 1cubr 25020 asin1 25072 dvatan 25113 log2cnv 25123 log2ublem3 25127 log2ub 25128 logfacbnd3 25400 bclbnd 25457 bpos1 25460 bposlem8 25468 lgsdilem 25501 lgsdir2lem1 25502 lgsdir2lem4 25505 lgsdir2lem5 25506 lgsdir2 25507 lgsdir 25509 2lgsoddprmlem3c 25589 dchrisum0flblem1 25649 rpvmasum2 25653 log2sumbnd 25685 ax5seglem7 26284 ex-fl 27879 ipasslem10 28266 hisubcomi 28533 normlem1 28539 normlem9 28547 norm-ii-i 28566 normsubi 28570 polid2i 28586 lnophmlem2 29448 lnfn0i 29473 nmopcoi 29526 unierri 29535 addltmulALT 29877 dpmul4 30184 sgnmul 31203 logdivsqrle 31330 hgt750lem 31331 hgt750lem2 31332 problem4 32159 quad3 32161 cnndvlem1 33110 sin2h 34008 poimirlem26 34045 cntotbnd 34203 sqdeccom12 38137 ex-decpmul 38140 areaquad 38742 coskpi2 40987 stoweidlem13 41139 wallispilem2 41192 wallispilem4 41194 wallispi2lem1 41197 dirkerper 41222 dirkertrigeqlem1 41224 dirkercncflem1 41229 sqwvfoura 41354 sqwvfourb 41355 fourierswlem 41356 fouriersw 41357 257prm 42476 fmtnofac1 42485 fmtno4prmfac 42487 fmtno4nprmfac193 42489 fmtno5faclem1 42494 fmtno5faclem2 42495 139prmALT 42514 127prm 42518 tgoldbach 42712 |
Copyright terms: Public domain | W3C validator |