Theorem 1t1e1 12343

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

Syntax hints:   = wceq 1540  (class class class)co 7387  1c1 11069   · cmul 11073

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-mulcom 11132  ax-mulass 11134  ax-distr 11135  ax-1rid 11138  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  neg1mulneg1e1  12394  addltmul  12418  1exp  14056  expge1  14064  mulexp  14066  mulexpz  14067  expaddz  14071  m1expeven  14074  sqrecii  14148  i4  14169  facp1  14243  hashf1  14422  binom  15796  prodf1  15857  prodfrec  15861  fprodmul  15926  fprodge1  15961  fallfac0  15994  binomfallfac  16007  pwp1fsum  16361  rpmul  16629  2503lem2  17108  2503lem3  17109  4001lem4  17114  abvtrivd  20741  pzriprng1ALT  21406  iimulcl  24833  dvexp  25857  dvef  25884  mulcxplem  26593  cxpmul2  26598  dvsqrt  26651  dvcnsqrt  26653  abscxpbnd  26663  1cubr  26752  dchrmulcl  27160  dchr1cl  27162  dchrinvcl  27164  lgslem3  27210  lgsval2lem  27218  lgsneg  27232  lgsdilem  27235  lgsdir  27243  lgsdi  27245  lgsquad2lem1  27295  lgsquad2lem2  27296  dchrisum0flblem2  27420  rpvmasum2  27423  mudivsum  27441  pntibndlem2  27502  axlowdimlem6  28874  hisubcomi  31033  lnophmlem2  31946  1nei  32660  1neg1t1neg1  32661  sgnmul  32760  hgt750lem2  34643  subfacval2  35174  faclim2  35735  knoppndvlem18  36517  lcmineqlem12  42028  pell1234qrmulcl  42843  pellqrex  42867  imsqrtvalex  43635  binomcxplemnotnn0  44345  dvnprodlem3  45946  stoweidlem13  46011  stoweidlem16  46014  wallispi  46068  wallispi2lem2  46070  2exp340mod341  47734  8exp8mod9  47737  nn0sumshdiglemB  48609