Theorem 1t1e1 12300

Description: 1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
1t1e1	⊢ (1 · 1) = 1

Proof of Theorem 1t1e1

Step	Hyp	Ref	Expression
1		ax-1cn 11082	. 2 ⊢ 1 ∈ ℂ
2	1	mulridi 11134	1 ⊢ (1 · 1) = 1

Syntax hints:   = wceq 1541  (class class class)co 7356  1c1 11025   · cmul 11029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-mulcl 11086  ax-mulcom 11088  ax-mulass 11090  ax-distr 11091  ax-1rid 11094  ax-cnre 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359

This theorem is referenced by:  neg1mulneg1e1  12351  addltmul  12375  1exp  14012  expge1  14020  mulexp  14022  mulexpz  14023  expaddz  14027  m1expeven  14030  sqrecii  14104  i4  14125  facp1  14199  hashf1  14378  binom  15751  prodf1  15812  prodfrec  15816  fprodmul  15881  fprodge1  15916  fallfac0  15949  binomfallfac  15962  pwp1fsum  16316  rpmul  16584  2503lem2  17063  2503lem3  17064  4001lem4  17069  abvtrivd  20763  pzriprng1ALT  21449  iimulcl  24887  dvexp  25911  dvef  25938  mulcxplem  26647  cxpmul2  26652  dvsqrt  26705  dvcnsqrt  26707  abscxpbnd  26717  1cubr  26806  dchrmulcl  27214  dchr1cl  27216  dchrinvcl  27218  lgslem3  27264  lgsval2lem  27272  lgsneg  27286  lgsdilem  27289  lgsdir  27297  lgsdi  27299  lgsquad2lem1  27349  lgsquad2lem2  27350  dchrisum0flblem2  27474  rpvmasum2  27477  mudivsum  27495  pntibndlem2  27556  axlowdimlem6  28969  hisubcomi  31128  lnophmlem2  32041  1nei  32765  1neg1t1neg1  32766  sgnmul  32865  hgt750lem2  34758  subfacval2  35330  faclim2  35891  knoppndvlem18  36672  lcmineqlem12  42233  pell1234qrmulcl  43039  pellqrex  43063  imsqrtvalex  43829  binomcxplemnotnn0  44539  dvnprodlem3  46134  stoweidlem13  46199  stoweidlem16  46202  wallispi  46256  wallispi2lem2  46258  2exp340mod341  47921  8exp8mod9  47924  nn0sumshdiglemB  48808