Theorem 1t1e1 12380

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 11172	. 2 ⊢ 1 ∈ ℂ
2	1	mulridi 11224	1 ⊢ (1 · 1) = 1

Syntax hints:   = wceq 1539  (class class class)co 7413  1c1 11115   · cmul 11119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-mulcl 11176  ax-mulcom 11178  ax-mulass 11180  ax-distr 11181  ax-1rid 11184  ax-cnre 11187

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7416

This theorem is referenced by:  neg1mulneg1e1  12431  addltmul  12454  1exp  14063  expge1  14071  mulexp  14073  mulexpz  14074  expaddz  14078  m1expeven  14081  sqrecii  14153  i4  14174  facp1  14244  hashf1  14424  binom  15782  prodf1  15843  prodfrec  15847  fprodmul  15910  fprodge1  15945  fallfac0  15978  binomfallfac  15991  pwp1fsum  16340  rpmul  16602  2503lem2  17077  2503lem3  17078  4001lem4  17083  abvtrivd  20593  pzriprng1ALT  21267  iimulcl  24682  dvexp  25704  dvef  25731  mulcxplem  26426  cxpmul2  26431  dvsqrt  26484  dvcnsqrt  26486  abscxpbnd  26495  1cubr  26581  dchrmulcl  26986  dchr1cl  26988  dchrinvcl  26990  lgslem3  27036  lgsval2lem  27044  lgsneg  27058  lgsdilem  27061  lgsdir  27069  lgsdi  27071  lgsquad2lem1  27121  lgsquad2lem2  27122  dchrisum0flblem2  27246  rpvmasum2  27249  mudivsum  27267  pntibndlem2  27328  axlowdimlem6  28470  hisubcomi  30622  lnophmlem2  31535  1nei  32226  1neg1t1neg1  32227  sgnmul  33837  hgt750lem2  33960  subfacval2  34474  faclim2  35020  knoppndvlem18  35710  lcmineqlem12  41213  pell1234qrmulcl  41897  pellqrex  41921  imsqrtvalex  42701  binomcxplemnotnn0  43419  dvnprodlem3  44964  stoweidlem13  45029  stoweidlem16  45032  wallispi  45086  wallispi2lem2  45088  2exp340mod341  46701  8exp8mod9  46704  nn0sumshdiglemB  47395