![]() |
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 10356 | . 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (1 · 𝐴) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1658 ∈ wcel 2166 (class class class)co 6906 ℂcc 10251 1c1 10254 · cmul 10258 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-resscn 10310 ax-1cn 10311 ax-icn 10312 ax-addcl 10313 ax-mulcl 10315 ax-mulcom 10317 ax-mulass 10319 ax-distr 10320 ax-1rid 10323 ax-cnre 10326 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ral 3123 df-rex 3124 df-rab 3127 df-v 3417 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4660 df-br 4875 df-iota 6087 df-fv 6132 df-ov 6909 |
This theorem is referenced by: 00id 10531 halfpm6th 11580 div4p1lem1div2 11614 3halfnz 11785 crreczi 13284 fac2 13360 hashxplem 13510 bpoly1 15155 bpoly2 15161 bpoly3 15162 bpoly4 15163 efival 15255 ef01bndlem 15287 3dvdsdec 15431 3dvds2dec 15432 odd2np1lem 15439 m1expo 15467 m1exp1 15468 nno 15473 divalglem5 15495 gcdaddmlem 15619 prmo2 16116 dec5nprm 16142 2exp8 16163 13prm 16189 23prm 16192 37prm 16194 43prm 16195 83prm 16196 139prm 16197 163prm 16198 317prm 16199 631prm 16200 1259lem2 16205 1259lem3 16206 1259lem4 16207 1259lem5 16208 2503lem1 16210 2503lem2 16211 2503lem3 16212 2503prm 16213 4001lem1 16214 4001lem2 16215 4001lem3 16216 4001lem4 16217 cnmsgnsubg 20283 sin2pim 24638 cos2pim 24639 sincosq3sgn 24653 sincosq4sgn 24654 tangtx 24658 sincosq1eq 24665 sincos4thpi 24666 sincos6thpi 24668 pige3 24670 abssinper 24671 ang180lem2 24951 ang180lem3 24952 1cubr 24983 asin1 25035 dvatan 25076 log2cnv 25085 log2ublem3 25089 log2ub 25090 logfacbnd3 25362 bclbnd 25419 bpos1 25422 bposlem8 25430 lgsdilem 25463 lgsdir2lem1 25464 lgsdir2lem4 25467 lgsdir2lem5 25468 lgsdir2 25469 lgsdir 25471 2lgsoddprmlem3c 25551 dchrisum0flblem1 25611 rpvmasum2 25615 log2sumbnd 25647 ax5seglem7 26235 ex-fl 27863 ipasslem10 28250 hisubcomi 28517 normlem1 28523 normlem9 28531 norm-ii-i 28550 normsubi 28554 polid2i 28570 lnophmlem2 29432 lnfn0i 29457 nmopcoi 29510 unierri 29519 addltmulALT 29861 dpmul4 30168 sgnmul 31151 logdivsqrle 31278 hgt750lem 31279 hgt750lem2 31280 problem4 32107 quad3 32109 cnndvlem1 33061 sin2h 33943 poimirlem26 33980 cntotbnd 34138 sqdeccom12 38065 ex-decpmul 38068 areaquad 38645 coskpi2 40873 stoweidlem13 41025 wallispilem2 41078 wallispilem4 41080 wallispi2lem1 41083 dirkerper 41108 dirkertrigeqlem1 41110 dirkercncflem1 41115 sqwvfoura 41240 sqwvfourb 41241 fourierswlem 41242 fouriersw 41243 257prm 42304 fmtnofac1 42313 fmtno4prmfac 42315 fmtno4nprmfac193 42317 fmtno5faclem1 42322 fmtno5faclem2 42323 139prmALT 42342 127prm 42346 tgoldbach 42536 |
Copyright terms: Public domain | W3C validator |