Theorem 1t1e1 12306

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 11140	1 ⊢ (1 · 1) = 1

Syntax hints:   = wceq 1542  (class class class)co 7360  1c1 11031   · cmul 11035

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 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 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 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7363

This theorem is referenced by:  neg1mulneg1e1  12357  addltmul  12381  1exp  14018  expge1  14026  mulexp  14028  mulexpz  14029  expaddz  14033  m1expeven  14036  sqrecii  14110  i4  14131  facp1  14205  hashf1  14384  binom  15757  prodf1  15818  prodfrec  15822  fprodmul  15887  fprodge1  15922  fallfac0  15955  binomfallfac  15968  pwp1fsum  16322  rpmul  16590  2503lem2  17069  2503lem3  17070  4001lem4  17075  abvtrivd  20769  pzriprng1ALT  21455  iimulcl  24893  dvexp  25917  dvef  25944  mulcxplem  26653  cxpmul2  26658  dvsqrt  26711  dvcnsqrt  26713  abscxpbnd  26723  1cubr  26812  dchrmulcl  27220  dchr1cl  27222  dchrinvcl  27224  lgslem3  27270  lgsval2lem  27278  lgsneg  27292  lgsdilem  27295  lgsdir  27303  lgsdi  27305  lgsquad2lem1  27355  lgsquad2lem2  27356  dchrisum0flblem2  27480  rpvmasum2  27483  mudivsum  27501  pntibndlem2  27562  axlowdimlem6  29024  hisubcomi  31183  lnophmlem2  32096  1nei  32818  1neg1t1neg1  32819  sgnmul  32918  hgt750lem2  34811  subfacval2  35383  faclim2  35944  knoppndvlem18  36731  lcmineqlem12  42362  pell1234qrmulcl  43164  pellqrex  43188  imsqrtvalex  43954  binomcxplemnotnn0  44664  dvnprodlem3  46259  stoweidlem13  46324  stoweidlem16  46327  wallispi  46381  wallispi2lem2  46383  2exp340mod341  48046  8exp8mod9  48049  nn0sumshdiglemB  48933