Theorem 1t1e1 12425

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

Syntax hints:   = wceq 1536  (class class class)co 7430  1c1 11153   · cmul 11157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-mulcl 11214  ax-mulcom 11216  ax-mulass 11218  ax-distr 11219  ax-1rid 11222  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  neg1mulneg1e1  12476  addltmul  12499  1exp  14128  expge1  14136  mulexp  14138  mulexpz  14139  expaddz  14143  m1expeven  14146  sqrecii  14218  i4  14239  facp1  14313  hashf1  14492  binom  15862  prodf1  15923  prodfrec  15927  fprodmul  15992  fprodge1  16027  fallfac0  16060  binomfallfac  16073  pwp1fsum  16424  rpmul  16692  2503lem2  17171  2503lem3  17172  4001lem4  17177  abvtrivd  20849  pzriprng1ALT  21524  iimulcl  24979  dvexp  26005  dvef  26032  mulcxplem  26740  cxpmul2  26745  dvsqrt  26798  dvcnsqrt  26800  abscxpbnd  26810  1cubr  26899  dchrmulcl  27307  dchr1cl  27309  dchrinvcl  27311  lgslem3  27357  lgsval2lem  27365  lgsneg  27379  lgsdilem  27382  lgsdir  27390  lgsdi  27392  lgsquad2lem1  27442  lgsquad2lem2  27443  dchrisum0flblem2  27567  rpvmasum2  27570  mudivsum  27588  pntibndlem2  27649  axlowdimlem6  28976  hisubcomi  31132  lnophmlem2  32045  1nei  32753  1neg1t1neg1  32754  sgnmul  34523  hgt750lem2  34645  subfacval2  35171  faclim2  35727  knoppndvlem18  36511  lcmineqlem12  42021  pell1234qrmulcl  42842  pellqrex  42866  imsqrtvalex  43635  binomcxplemnotnn0  44351  dvnprodlem3  45903  stoweidlem13  45968  stoweidlem16  45971  wallispi  46025  wallispi2lem2  46027  2exp340mod341  47657  8exp8mod9  47660  nn0sumshdiglemB  48469