Theorem 1t1e1 12370

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

Syntax hints:   = wceq 1541  (class class class)co 7405  1c1 11107   · cmul 11111

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-mulcl 11168  ax-mulcom 11170  ax-mulass 11172  ax-distr 11173  ax-1rid 11176  ax-cnre 11179

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408

This theorem is referenced by:  neg1mulneg1e1  12421  addltmul  12444  1exp  14053  expge1  14061  mulexp  14063  mulexpz  14064  expaddz  14068  m1expeven  14071  sqrecii  14143  i4  14164  facp1  14234  hashf1  14414  binom  15772  prodf1  15833  prodfrec  15837  fprodmul  15900  fprodge1  15935  fallfac0  15968  binomfallfac  15981  pwp1fsum  16330  rpmul  16592  2503lem2  17067  2503lem3  17068  4001lem4  17073  abvtrivd  20440  iimulcl  24444  dvexp  25461  dvef  25488  mulcxplem  26183  cxpmul2  26188  dvsqrt  26239  dvcnsqrt  26241  abscxpbnd  26250  1cubr  26336  dchrmulcl  26741  dchr1cl  26743  dchrinvcl  26745  lgslem3  26791  lgsval2lem  26799  lgsneg  26813  lgsdilem  26816  lgsdir  26824  lgsdi  26826  lgsquad2lem1  26876  lgsquad2lem2  26877  dchrisum0flblem2  27001  rpvmasum2  27004  mudivsum  27022  pntibndlem2  27083  axlowdimlem6  28194  hisubcomi  30344  lnophmlem2  31257  1nei  31948  1neg1t1neg1  31949  sgnmul  33529  hgt750lem2  33652  subfacval2  34166  faclim2  34706  knoppndvlem18  35393  lcmineqlem12  40893  pell1234qrmulcl  41578  pellqrex  41602  imsqrtvalex  42382  binomcxplemnotnn0  43100  dvnprodlem3  44650  stoweidlem13  44715  stoweidlem16  44718  wallispi  44772  wallispi2lem2  44774  2exp340mod341  46387  8exp8mod9  46390  nn0sumshdiglemB  47259