Theorem 1t1e1 12330

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

Syntax hints:   = wceq 1547  (class class class)co 7357  1c1 11031   · cmul 11035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-mulcl 11092  ax-mulcom 11094  ax-mulass 11096  ax-distr 11097  ax-1rid 11100  ax-cnre 11103

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4263  df-if 4456  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-br 5074  df-iota 6442  df-fv 6494  df-ov 7360

This theorem is referenced by:  neg1mulneg1e1  12381  addltmul  12405  1exp  14045  expge1  14053  mulexp  14055  mulexpz  14056  expaddz  14060  m1expeven  14063  sqrecii  14137  i4  14158  facp1  14232  hashf1  14411  binom  15787  prodf1  15848  prodfrec  15852  fprodmul  15917  fprodge1  15952  fallfac0  15985  binomfallfac  15998  pwp1fsum  16352  rpmul  16620  2503lem2  17100  2503lem3  17101  4001lem4  17106  abvtrivd  20805  pzriprng1ALT  21472  iimulcl  24923  dvexp  25939  dvef  25966  mulcxplem  26667  cxpmul2  26672  dvsqrt  26725  dvcnsqrt  26727  abscxpbnd  26736  1cubr  26825  dchrmulcl  27231  dchr1cl  27233  dchrinvcl  27235  lgslem3  27281  lgsval2lem  27289  lgsneg  27303  lgsdilem  27306  lgsdir  27314  lgsdi  27316  lgsquad2lem1  27366  lgsquad2lem2  27367  dchrisum0flblem2  27491  rpvmasum2  27494  mudivsum  27512  pntibndlem2  27573  axlowdimlem6  29035  hisubcomi  31194  lnophmlem2  32107  1nei  32830  1neg1t1neg1  32831  sgnmul  32928  hgt750lem2  34845  subfacval2  35424  faclim2  35985  knoppndvlem18  36844  lcmineqlem12  42534  pell1234qrmulcl  43309  pellqrex  43333  imsqrtvalex  44099  binomcxplemnotnn0  44809  dvnprodlem3  46399  stoweidlem13  46464  stoweidlem16  46467  wallispi  46521  wallispi2lem2  46523  2exp340mod341  48232  8exp8mod9  48235  nn0sumshdiglemB  49119