Theorem 1t1e1 11607

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 10391	. 2 ⊢ 1 ∈ ℂ
2	1	mulid1i 10442	1 ⊢ (1 · 1) = 1

Syntax hints:   = wceq 1507  (class class class)co 6974  1c1 10334   · cmul 10338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744  ax-resscn 10390  ax-1cn 10391  ax-icn 10392  ax-addcl 10393  ax-mulcl 10395  ax-mulcom 10397  ax-mulass 10399  ax-distr 10400  ax-1rid 10403  ax-cnre 10406

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4709  df-br 4926  df-iota 6149  df-fv 6193  df-ov 6977

This theorem is referenced by:  neg1mulneg1e1  11658  addltmul  11681  1exp  13271  expge1  13279  mulexp  13281  mulexpz  13282  expaddz  13286  m1expeven  13289  sqrecii  13359  i4  13380  facp1  13451  hashf1  13626  binom  15043  prodf1  15105  prodfrec  15109  fprodmul  15172  fprodge1  15207  fallfac0  15240  binomfallfac  15253  pwp1fsum  15600  rpmul  15857  2503lem2  16325  2503lem3  16326  4001lem4  16331  abvtrivd  19345  iimulcl  23256  dvexp  24265  dvef  24292  mulcxplem  24980  cxpmul2  24985  dvsqrt  25036  dvcnsqrt  25038  abscxpbnd  25047  1cubr  25133  dchrmulcl  25539  dchr1cl  25541  dchrinvcl  25543  lgslem3  25589  lgsval2lem  25597  lgsneg  25611  lgsdilem  25614  lgsdir  25622  lgsdi  25624  lgsquad2lem1  25674  lgsquad2lem2  25675  dchrisum0flblem2  25799  rpvmasum2  25802  mudivsum  25820  pntibndlem2  25881  axlowdimlem6  26448  hisubcomi  28672  lnophmlem2  29587  1nei  30245  1neg1t1neg1  30246  sgnmul  31475  hgt750lem2  31600  subfacval2  32048  faclim2  32529  knoppndvlem18  33417  pell1234qrmulcl  38877  pellqrex  38901  binomcxplemnotnn0  40133  dvnprodlem3  41688  stoweidlem13  41754  stoweidlem16  41757  wallispi  41811  wallispi2lem2  41813  2exp340mod341  43291  8exp8mod9  43294  nn0sumshdiglemB  44073