Theorem 1t1e1 12374

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

Syntax hints:   = wceq 1542  (class class class)co 7409  1c1 11111   · cmul 11115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-mulcl 11172  ax-mulcom 11174  ax-mulass 11176  ax-distr 11177  ax-1rid 11180  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  neg1mulneg1e1  12425  addltmul  12448  1exp  14057  expge1  14065  mulexp  14067  mulexpz  14068  expaddz  14072  m1expeven  14075  sqrecii  14147  i4  14168  facp1  14238  hashf1  14418  binom  15776  prodf1  15837  prodfrec  15841  fprodmul  15904  fprodge1  15939  fallfac0  15972  binomfallfac  15985  pwp1fsum  16334  rpmul  16596  2503lem2  17071  2503lem3  17072  4001lem4  17077  abvtrivd  20448  iimulcl  24453  dvexp  25470  dvef  25497  mulcxplem  26192  cxpmul2  26197  dvsqrt  26250  dvcnsqrt  26252  abscxpbnd  26261  1cubr  26347  dchrmulcl  26752  dchr1cl  26754  dchrinvcl  26756  lgslem3  26802  lgsval2lem  26810  lgsneg  26824  lgsdilem  26827  lgsdir  26835  lgsdi  26837  lgsquad2lem1  26887  lgsquad2lem2  26888  dchrisum0flblem2  27012  rpvmasum2  27015  mudivsum  27033  pntibndlem2  27094  axlowdimlem6  28205  hisubcomi  30357  lnophmlem2  31270  1nei  31961  1neg1t1neg1  31962  sgnmul  33541  hgt750lem2  33664  subfacval2  34178  faclim2  34718  knoppndvlem18  35405  lcmineqlem12  40905  pell1234qrmulcl  41593  pellqrex  41617  imsqrtvalex  42397  binomcxplemnotnn0  43115  dvnprodlem3  44664  stoweidlem13  44729  stoweidlem16  44732  wallispi  44786  wallispi2lem2  44788  2exp340mod341  46401  8exp8mod9  46404  pzriprng1ALT  46820  nn0sumshdiglemB  47306