Theorem 1t1e1 11787

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 10584	. 2 ⊢ 1 ∈ ℂ
2	1	mulid1i 10634	1 ⊢ (1 · 1) = 1

Syntax hints:   = wceq 1538  (class class class)co 7135  1c1 10527   · cmul 10531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  neg1mulneg1e1  11838  addltmul  11861  1exp  13454  expge1  13462  mulexp  13464  mulexpz  13465  expaddz  13469  m1expeven  13472  sqrecii  13542  i4  13563  facp1  13634  hashf1  13811  binom  15177  prodf1  15239  prodfrec  15243  fprodmul  15306  fprodge1  15341  fallfac0  15374  binomfallfac  15387  pwp1fsum  15732  rpmul  15993  2503lem2  16463  2503lem3  16464  4001lem4  16469  abvtrivd  19604  iimulcl  23542  dvexp  24556  dvef  24583  mulcxplem  25275  cxpmul2  25280  dvsqrt  25331  dvcnsqrt  25333  abscxpbnd  25342  1cubr  25428  dchrmulcl  25833  dchr1cl  25835  dchrinvcl  25837  lgslem3  25883  lgsval2lem  25891  lgsneg  25905  lgsdilem  25908  lgsdir  25916  lgsdi  25918  lgsquad2lem1  25968  lgsquad2lem2  25969  dchrisum0flblem2  26093  rpvmasum2  26096  mudivsum  26114  pntibndlem2  26175  axlowdimlem6  26741  hisubcomi  28887  lnophmlem2  29800  1nei  30498  1neg1t1neg1  30499  sgnmul  31910  hgt750lem2  32033  subfacval2  32547  faclim2  33093  knoppndvlem18  33981  lcmineqlem12  39328  3lexlogpow5ineq1  39341  pell1234qrmulcl  39796  pellqrex  39820  imsqrtvalex  40346  binomcxplemnotnn0  41060  dvnprodlem3  42590  stoweidlem13  42655  stoweidlem16  42658  wallispi  42712  wallispi2lem2  42714  2exp340mod341  44251  8exp8mod9  44254  nn0sumshdiglemB  45034