Theorem 2t2e4 12316

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 12232	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12290	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12287	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2760	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1542  (class class class)co 7368   + caddc 11041   · cmul 11043  2c2 12212  4c4 12214

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 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-1rid 11108  ax-cnre 11111

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-2 12220  df-3 12221  df-4 12222

This theorem is referenced by:  4div2e2  12322  div4p1lem1div2  12408  3halfnz  12583  decbin0  12759  fldiv4lem1div2uz2  13768  sq2  14132  sq4e2t8  14134  discr  14175  sqoddm1div8  14178  faclbnd2  14226  4bc2eq6  14264  amgm2  15305  bpoly3  15993  sin4lt0  16132  z4even  16311  flodddiv4  16354  flodddiv4t2lthalf  16357  4nprm  16634  2exp4  17024  2exp16  17030  5prm  17048  631prm  17066  1259lem1  17070  1259lem4  17073  2503lem1  17076  2503lem2  17077  2503lem3  17078  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001prm  17084  pcoass  24992  minveclem2  25394  uniioombllem5  25556  uniioombl  25558  dveflem  25951  pilem2  26430  sinhalfpilem  26440  sincosq1lem  26474  tangtx  26482  sincos4thpi  26490  heron  26816  quad2  26817  dquartlem1  26829  dquart  26831  quart1  26834  atan1  26906  log2ublem3  26926  log2ub  26927  chtub  27191  bclbnd  27259  bpos1  27262  bposlem2  27264  bposlem6  27268  bposlem9  27271  gausslemma2dlem3  27347  m1lgs  27367  2lgslem1a2  27369  2lgslem3a  27375  2lgslem3b  27376  2lgslem3c  27377  2lgslem3d  27378  pntibndlem2  27570  pntlemg  27577  pntlemr  27581  ex-fl  30534  minvecolem2  30963  polid2i  31245  binom2subadd  32832  quad3d  32840  quad3  35886  420lcm8e840  42381  3exp7  42423  3lexlogpow5ineq1  42424  3lexlogpow2ineq2  42429  3lexlogpow5ineq5  42430  aks4d1p1p2  42440  aks4d1p1  42446  2ap1caineq  42515  cxpi11d  42713  flt4lem  43003  3cubeslem3l  43043  3cubeslem3r  43044  wallispi2lem1  46429  wallispi2lem2  46430  stirlinglem3  46434  stirlinglem10  46441  2ltceilhalf  47688  ceil5half3  47700  modmkpkne  47721  fmtnorec4  47909  2exp340mod341  48093  8exp8mod9  48096  ackval2012  49051