Theorem 1t1e1 12428

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

Syntax hints:   = wceq 1540  (class class class)co 7431  1c1 11156   · cmul 11160

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-mulcom 11219  ax-mulass 11221  ax-distr 11222  ax-1rid 11225  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  neg1mulneg1e1  12479  addltmul  12502  1exp  14132  expge1  14140  mulexp  14142  mulexpz  14143  expaddz  14147  m1expeven  14150  sqrecii  14222  i4  14243  facp1  14317  hashf1  14496  binom  15866  prodf1  15927  prodfrec  15931  fprodmul  15996  fprodge1  16031  fallfac0  16064  binomfallfac  16077  pwp1fsum  16428  rpmul  16696  2503lem2  17175  2503lem3  17176  4001lem4  17181  abvtrivd  20833  pzriprng1ALT  21507  iimulcl  24966  dvexp  25991  dvef  26018  mulcxplem  26726  cxpmul2  26731  dvsqrt  26784  dvcnsqrt  26786  abscxpbnd  26796  1cubr  26885  dchrmulcl  27293  dchr1cl  27295  dchrinvcl  27297  lgslem3  27343  lgsval2lem  27351  lgsneg  27365  lgsdilem  27368  lgsdir  27376  lgsdi  27378  lgsquad2lem1  27428  lgsquad2lem2  27429  dchrisum0flblem2  27553  rpvmasum2  27556  mudivsum  27574  pntibndlem2  27635  axlowdimlem6  28962  hisubcomi  31123  lnophmlem2  32036  1nei  32747  1neg1t1neg1  32748  sgnmul  34545  hgt750lem2  34667  subfacval2  35192  faclim2  35748  knoppndvlem18  36530  lcmineqlem12  42041  pell1234qrmulcl  42866  pellqrex  42890  imsqrtvalex  43659  binomcxplemnotnn0  44375  dvnprodlem3  45963  stoweidlem13  46028  stoweidlem16  46031  wallispi  46085  wallispi2lem2  46087  2exp340mod341  47720  8exp8mod9  47723  nn0sumshdiglemB  48541