Theorem 1t1e1 12349

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

Syntax hints:   = wceq 1540  (class class class)co 7389  1c1 11075   · cmul 11079

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 2702  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-mulcl 11136  ax-mulcom 11138  ax-mulass 11140  ax-distr 11141  ax-1rid 11144  ax-cnre 11147

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 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-iota 6466  df-fv 6521  df-ov 7392

This theorem is referenced by:  neg1mulneg1e1  12400  addltmul  12424  1exp  14062  expge1  14070  mulexp  14072  mulexpz  14073  expaddz  14077  m1expeven  14080  sqrecii  14154  i4  14175  facp1  14249  hashf1  14428  binom  15802  prodf1  15863  prodfrec  15867  fprodmul  15932  fprodge1  15967  fallfac0  16000  binomfallfac  16013  pwp1fsum  16367  rpmul  16635  2503lem2  17114  2503lem3  17115  4001lem4  17120  abvtrivd  20747  pzriprng1ALT  21412  iimulcl  24839  dvexp  25863  dvef  25890  mulcxplem  26599  cxpmul2  26604  dvsqrt  26657  dvcnsqrt  26659  abscxpbnd  26669  1cubr  26758  dchrmulcl  27166  dchr1cl  27168  dchrinvcl  27170  lgslem3  27216  lgsval2lem  27224  lgsneg  27238  lgsdilem  27241  lgsdir  27249  lgsdi  27251  lgsquad2lem1  27301  lgsquad2lem2  27302  dchrisum0flblem2  27426  rpvmasum2  27429  mudivsum  27447  pntibndlem2  27508  axlowdimlem6  28880  hisubcomi  31039  lnophmlem2  31952  1nei  32666  1neg1t1neg1  32667  sgnmul  32766  hgt750lem2  34649  subfacval2  35174  faclim2  35730  knoppndvlem18  36512  lcmineqlem12  42023  pell1234qrmulcl  42836  pellqrex  42860  imsqrtvalex  43628  binomcxplemnotnn0  44338  dvnprodlem3  45939  stoweidlem13  46004  stoweidlem16  46007  wallispi  46061  wallispi2lem2  46063  2exp340mod341  47724  8exp8mod9  47727  nn0sumshdiglemB  48599