Theorem 1t1e1 12338

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

Syntax hints:   = wceq 1542  (class class class)co 7367  1c1 11039   · cmul 11043

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 2708  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-mulcom 11102  ax-mulass 11104  ax-distr 11105  ax-1rid 11108  ax-cnre 11111

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 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  neg1mulneg1e1  12389  addltmul  12413  1exp  14053  expge1  14061  mulexp  14063  mulexpz  14064  expaddz  14068  m1expeven  14071  sqrecii  14145  i4  14166  facp1  14240  hashf1  14419  binom  15795  prodf1  15856  prodfrec  15860  fprodmul  15925  fprodge1  15960  fallfac0  15993  binomfallfac  16006  pwp1fsum  16360  rpmul  16628  2503lem2  17108  2503lem3  17109  4001lem4  17114  abvtrivd  20809  pzriprng1ALT  21476  iimulcl  24904  dvexp  25920  dvef  25947  mulcxplem  26648  cxpmul2  26653  dvsqrt  26706  dvcnsqrt  26708  abscxpbnd  26717  1cubr  26806  dchrmulcl  27212  dchr1cl  27214  dchrinvcl  27216  lgslem3  27262  lgsval2lem  27270  lgsneg  27284  lgsdilem  27287  lgsdir  27295  lgsdi  27297  lgsquad2lem1  27347  lgsquad2lem2  27348  dchrisum0flblem2  27472  rpvmasum2  27475  mudivsum  27493  pntibndlem2  27554  axlowdimlem6  29016  hisubcomi  31175  lnophmlem2  32088  1nei  32810  1neg1t1neg1  32811  sgnmul  32908  hgt750lem2  34796  subfacval2  35369  faclim2  35930  knoppndvlem18  36789  lcmineqlem12  42479  pell1234qrmulcl  43283  pellqrex  43307  imsqrtvalex  44073  binomcxplemnotnn0  44783  dvnprodlem3  46376  stoweidlem13  46441  stoweidlem16  46444  wallispi  46498  wallispi2lem2  46500  2exp340mod341  48209  8exp8mod9  48212  nn0sumshdiglemB  49096