Theorem mulridi 11241

Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)

Hypothesis

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
mulridi	⊢ (𝐴 · 1) = 𝐴

Proof of Theorem mulridi

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		mulrid 11234	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 · 1) = 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126  1c1 11129   · cmul 11133

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-mulcl 11190  ax-mulcom 11192  ax-mulass 11194  ax-distr 11195  ax-1rid 11198  ax-cnre 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420

This theorem is used by:  addrid  11418  0lt1  11764  muleqadd  11886  1t1e1  12430  2t1e2  12431  3t1e3  12433  9p1e10  12742  numltc  12771  numsucc  12785  dec10p  12788  numadd  12792  numaddc  12793  11multnc  12813  4t3lem  12842  5t2e10  12845  9t11e99OLD  12876  nn0opthlem1  14336  faclbnd4lem1  14361  sgnmul  15184  rei  15247  imi  15248  cji  15250  sqrtm1  15366  0.999...  15974  efival  16246  ef01bndlem  16278  5ndvds6  16510  3lcm2e6  16829  decsplit0b  17177  2exp8  17186  37prm  17219  43prm  17220  83prm  17221  139prm  17222  163prm  17223  317prm  17224  1259lem1  17229  1259lem2  17230  1259lem3  17231  1259lem4  17232  1259lem5  17233  2503lem1  17235  2503lem2  17236  2503prm  17238  4001lem1  17239  4001lem2  17240  4001lem3  17241  cnmsgnsubg  21796  mdetralt  22836  dveflem  26213  dvsincos  26215  efhalfpi  26716  pige3ALT  26765  cosne0  26774  efif1olem4  26790  logf1o2  26895  asin1  27139  dvatan  27180  log2ublem3  27193  log2ub  27194  birthday  27199  basellem9  27333  ppiub  27448  chtub  27456  bposlem8  27535  lgsdir2  27574  mulog2sumlem2  27779  pntlemb  27841  avril1  30951  ipidsq  31199  nmopadjlem  32578  nmopcoadji  32590  unierri  32593  signswch  35077  itgexpif  35122  reprlt  35135  breprexp  35149  hgt750lem  35167  hgt750lem2  35168  circum  36261  dvasin  38461  3lexlogpow5ineq1  42928  3lexlogpow5ineq5  42934  aks4d1p1  42950  235t711  43188  ex-decpmul  43189  it1ei  43199  sqrtcval2  44490  resqrtvalex  44493  imsqrtvalex  44494  inductionexd  45003  xralrple3  46211  wallispi  46906  wallispi2lem2  46908  stirlinglem1  46910  dirkertrigeqlem3  46936  goldpolyfactor  47753  goldratval  47762  modm1p1ne  48272  257prm  48472  fmtno4prmfac193  48484  fmtno5fac  48493  139prmALT  48507  127prm  48510  2exp340mod341  48657