Theorem 1t1e1 12333

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

Syntax hints:   = wceq 1542  (class class class)co 7362  1c1 11034   · cmul 11038

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-mulcl 11095  ax-mulcom 11097  ax-mulass 11099  ax-distr 11100  ax-1rid 11103  ax-cnre 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6450  df-fv 6502  df-ov 7365

This theorem is referenced by:  neg1mulneg1e1  12384  addltmul  12408  1exp  14048  expge1  14056  mulexp  14058  mulexpz  14059  expaddz  14063  m1expeven  14066  sqrecii  14140  i4  14161  facp1  14235  hashf1  14414  binom  15790  prodf1  15851  prodfrec  15855  fprodmul  15920  fprodge1  15955  fallfac0  15988  binomfallfac  16001  pwp1fsum  16355  rpmul  16623  2503lem2  17103  2503lem3  17104  4001lem4  17109  abvtrivd  20804  pzriprng1ALT  21490  iimulcl  24918  dvexp  25934  dvef  25961  mulcxplem  26665  cxpmul2  26670  dvsqrt  26723  dvcnsqrt  26725  abscxpbnd  26734  1cubr  26823  dchrmulcl  27230  dchr1cl  27232  dchrinvcl  27234  lgslem3  27280  lgsval2lem  27288  lgsneg  27302  lgsdilem  27305  lgsdir  27313  lgsdi  27315  lgsquad2lem1  27365  lgsquad2lem2  27366  dchrisum0flblem2  27490  rpvmasum2  27493  mudivsum  27511  pntibndlem2  27572  axlowdimlem6  29034  hisubcomi  31194  lnophmlem2  32107  1nei  32829  1neg1t1neg1  32830  sgnmul  32927  hgt750lem2  34816  subfacval2  35389  faclim2  35950  knoppndvlem18  36809  lcmineqlem12  42497  pell1234qrmulcl  43305  pellqrex  43329  imsqrtvalex  44095  binomcxplemnotnn0  44805  dvnprodlem3  46398  stoweidlem13  46463  stoweidlem16  46466  wallispi  46520  wallispi2lem2  46522  2exp340mod341  48225  8exp8mod9  48228  nn0sumshdiglemB  49112