Theorem mullidi 11295

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

Hypothesis

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
mullidi	⊢ (1 · 𝐴) = 𝐴

Proof of Theorem mullidi

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179  1c1 11182   · cmul 11186

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 2733  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-mulcl 11243  ax-mulcom 11245  ax-mulass 11247  ax-distr 11248  ax-1rid 11251  ax-cnre 11254

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 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415

This theorem is used by:  00id  11466  div4p1lem1div2  12582  3halfnz  12759  crreczi  14352  fac2  14403  hashxplem  14558  sgnmul  15240  bpoly1  16197  bpoly2  16203  bpoly3  16204  bpoly4  16205  efival  16300  ef01bndlem  16332  3dvdsdec  16482  3dvds2dec  16483  odd2np1lem  16490  m1expo  16525  m1exp1  16526  nno  16532  divalglem5  16547  gcdaddmlem  16676  prmo2  17198  dec5nprm  17224  2exp8  17246  13prm  17274  23prm  17277  37prm  17279  43prm  17280  83prm  17281  139prm  17282  163prm  17283  317prm  17284  631prm  17285  1259lem2  17290  1259lem3  17291  1259lem4  17292  1259lem5  17293  2503lem1  17295  2503lem2  17296  2503lem3  17297  2503prm  17298  4001lem1  17299  4001lem2  17300  4001lem3  17301  4001lem4  17302  cnmsgnsubg  21863  iaa  26633  sin2pim  26796  cos2pim  26797  sincosq3sgn  26811  sincosq4sgn  26812  tangtx  26816  sincosq1eq  26823  sincos4thpi  26824  sincos6thpi  26826  pige3ALT  26830  abssinper  26831  ang180lem2  27120  ang180lem3  27121  1cubr  27152  asin1  27204  dvatan  27245  log2cnv  27254  log2ublem3  27258  log2ub  27259  logfacbnd3  27532  bclbnd  27589  bpos1  27592  bposlem8  27600  lgsdilem  27633  lgsdir2lem1  27634  lgsdir2lem4  27637  lgsdir2lem5  27638  lgsdir2  27639  lgsdir  27641  2lgsoddprmlem3c  27721  dchrisum0flblem1  27817  rpvmasum2  27821  log2sumbnd  27853  ax5seglem7  29495  ex-fl  31030  ipasslem10  31423  hisubcomi  31688  normlem1  31694  normlem9  31702  norm-ii-i  31721  normsubi  31725  polid2i  31741  lnophmlem2  32601  lnfn0i  32626  nmopcoi  32679  unierri  32688  addltmulALT  33030  dpmul4  33462  iconstr  34380  cos9thpiminplylem5  34400  logdivsqrle  35262  hgt750lem  35263  hgt750lem2  35264  problem4  36402  quad3  36404  cnndvlem1  37373  sin2h  38501  poimirlem26  38532  cntotbnd  38698  60gcd6e6  43022  12lcm5e60  43026  60lcm7e420  43028  3lexlogpow5ineq1  43072  3lexlogpow5ineq5  43078  sqdeccom12  43314  ex-decpmul  43331  1tiei  43342  sin2t3rdpi  43372  cos2t3rdpi  43373  areaquad  44176  resqrtvalex  44604  imsqrtvalex  44605  coskpi2  46820  stoweidlem13  46967  wallispilem2  47020  wallispilem4  47022  wallispi2lem1  47025  dirkerper  47050  dirkertrigeqlem1  47052  dirkercncflem1  47057  sqwvfoura  47182  sqwvfourb  47183  fourierswlem  47184  fouriersw  47185  cos5t  47869  goldpolyfactor  47871  goldratval  47880  lamberte  47882  rehalfge1  48353  257prm  48590  fmtnofac1  48599  fmtno4prmfac  48601  fmtno4nprmfac193  48603  fmtno5faclem1  48608  fmtno5faclem2  48609  139prmALT  48625  127prm  48628  11t31e341  48774  2exp340mod341  48775  nfermltl8rev  48784  tgoldbach  48859