Theorem 2t2e4 12334

Description: 2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.)

Assertion

Ref	Expression
2t2e4	⊢ (2 · 2) = 4

Proof of Theorem 2t2e4

Step	Hyp	Ref	Expression
1		2cn 12250	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12308	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12305	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2760	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1542  (class class class)co 7361   + caddc 11035   · cmul 11037  2c2 12230  4c4 12232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-mulcl 11094  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-1rid 11102  ax-cnre 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-2 12238  df-3 12239  df-4 12240

This theorem is referenced by:  4div2e2  12340  div4p1lem1div2  12426  3halfnz  12602  decbin0  12778  fldiv4lem1div2uz2  13789  sq2  14153  sq4e2t8  14155  discr  14196  sqoddm1div8  14199  faclbnd2  14247  4bc2eq6  14285  amgm2  15326  bpoly3  16017  sin4lt0  16156  z4even  16335  flodddiv4  16378  flodddiv4t2lthalf  16381  4nprm  16658  2exp4  17049  2exp16  17055  5prm  17073  631prm  17091  1259lem1  17095  1259lem4  17098  2503lem1  17101  2503lem2  17102  2503lem3  17103  4001lem1  17105  4001lem2  17106  4001lem3  17107  4001prm  17109  pcoass  25004  minveclem2  25406  uniioombllem5  25567  uniioombl  25569  dveflem  25959  pilem2  26433  sinhalfpilem  26443  sincosq1lem  26477  tangtx  26485  sincos4thpi  26493  heron  26818  quad2  26819  dquartlem1  26831  dquart  26833  quart1  26836  atan1  26908  log2ublem3  26928  log2ub  26929  chtub  27192  bclbnd  27260  bpos1  27263  bposlem2  27265  bposlem6  27269  bposlem9  27272  gausslemma2dlem3  27348  m1lgs  27368  2lgslem1a2  27370  2lgslem3a  27376  2lgslem3b  27377  2lgslem3c  27378  2lgslem3d  27379  pntibndlem2  27571  pntlemg  27578  pntlemr  27582  ex-fl  30535  minvecolem2  30964  polid2i  31246  binom2subadd  32832  quad3d  32840  quad3  35871  420lcm8e840  42467  3exp7  42509  3lexlogpow5ineq1  42510  3lexlogpow2ineq2  42515  3lexlogpow5ineq5  42516  aks4d1p1p2  42526  aks4d1p1  42532  2ap1caineq  42601  cxpi11d  42792  flt4lem  43095  3cubeslem3l  43135  3cubeslem3r  43136  wallispi2lem1  46520  wallispi2lem2  46521  stirlinglem3  46525  stirlinglem10  46532  sin5tlem2  47341  2ltceilhalf  47795  ceil5half3  47809  modmkpkne  47830  fmtnorec4  48027  nprmdvdsfacm1lem4  48101  ppivalnn4  48105  2exp340mod341  48224  8exp8mod9  48227  ackval2012  49182