Theorem 1t1e1 11800

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

Syntax hints:   = wceq 1537  (class class class)co 7156  1c1 10538   · cmul 10542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-mulcl 10599  ax-mulcom 10601  ax-mulass 10603  ax-distr 10604  ax-1rid 10607  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  neg1mulneg1e1  11851  addltmul  11874  1exp  13459  expge1  13467  mulexp  13469  mulexpz  13470  expaddz  13474  m1expeven  13477  sqrecii  13547  i4  13568  facp1  13639  hashf1  13816  binom  15185  prodf1  15247  prodfrec  15251  fprodmul  15314  fprodge1  15349  fallfac0  15382  binomfallfac  15395  pwp1fsum  15742  rpmul  16003  2503lem2  16471  2503lem3  16472  4001lem4  16477  abvtrivd  19611  iimulcl  23541  dvexp  24550  dvef  24577  mulcxplem  25267  cxpmul2  25272  dvsqrt  25323  dvcnsqrt  25325  abscxpbnd  25334  1cubr  25420  dchrmulcl  25825  dchr1cl  25827  dchrinvcl  25829  lgslem3  25875  lgsval2lem  25883  lgsneg  25897  lgsdilem  25900  lgsdir  25908  lgsdi  25910  lgsquad2lem1  25960  lgsquad2lem2  25961  dchrisum0flblem2  26085  rpvmasum2  26088  mudivsum  26106  pntibndlem2  26167  axlowdimlem6  26733  hisubcomi  28881  lnophmlem2  29794  1nei  30472  1neg1t1neg1  30473  sgnmul  31800  hgt750lem2  31923  subfacval2  32434  faclim2  32980  knoppndvlem18  33868  pell1234qrmulcl  39472  pellqrex  39496  binomcxplemnotnn0  40708  dvnprodlem3  42253  stoweidlem13  42318  stoweidlem16  42321  wallispi  42375  wallispi2lem2  42377  2exp340mod341  43918  8exp8mod9  43921  nn0sumshdiglemB  44700