Theorem 1t1e1 11175

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

Syntax hints:   = wceq 1483  (class class class)co 6650  1c1 9937   · cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-mulcl 9998  ax-mulcom 10000  ax-mulass 10002  ax-distr 10003  ax-1rid 10006  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  neg1mulneg1e1  11245  addltmul  11268  1exp  12889  expge1  12897  mulexp  12899  mulexpz  12900  expaddz  12904  m1expeven  12907  sqrecii  12946  i4  12967  facp1  13065  hashf1  13241  binom  14562  prodf1  14623  prodfrec  14627  fprodmul  14690  fprodge1  14726  fallfac0  14759  binomfallfac  14772  pwp1fsum  15114  rpmul  15373  2503lem2  15845  2503lem3  15846  4001lem4  15851  abvtrivd  18840  iimulcl  22736  dvexp  23716  dvef  23743  mulcxplem  24430  cxpmul2  24435  dvsqrt  24483  dvcnsqrt  24485  abscxpbnd  24494  1cubr  24569  dchrmulcl  24974  dchr1cl  24976  dchrinvcl  24978  lgslem3  25024  lgsval2lem  25032  lgsneg  25046  lgsdilem  25049  lgsdir  25057  lgsdi  25059  lgsquad2lem1  25109  lgsquad2lem2  25110  dchrisum0flblem2  25198  rpvmasum2  25201  mudivsum  25219  pntibndlem2  25280  axlowdimlem6  25827  hisubcomi  27961  lnophmlem2  28876  1neg1t1neg1  29514  sgnmul  30604  hgt750lem2  30730  subfacval2  31169  faclim2  31634  knoppndvlem18  32520  pell1234qrmulcl  37419  pellqrex  37443  binomcxplemnotnn0  38555  dvnprodlem3  40163  stoweidlem13  40230  stoweidlem16  40233  wallispi  40287  wallispi2lem2  40289  nn0sumshdiglemB  42414