Theorem 2t2e4 12302

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 12218	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12276	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12273	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2757	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1541  (class class class)co 7356   + caddc 11027   · cmul 11029  2c2 12198  4c4 12200

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-mulcl 11086  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-1rid 11094  ax-cnre 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-2 12206  df-3 12207  df-4 12208

This theorem is referenced by:  4div2e2  12308  div4p1lem1div2  12394  3halfnz  12569  decbin0  12745  fldiv4lem1div2uz2  13754  sq2  14118  sq4e2t8  14120  discr  14161  sqoddm1div8  14164  faclbnd2  14212  4bc2eq6  14250  amgm2  15291  bpoly3  15979  sin4lt0  16118  z4even  16297  flodddiv4  16340  flodddiv4t2lthalf  16343  4nprm  16620  2exp4  17010  2exp16  17016  5prm  17034  631prm  17052  1259lem1  17056  1259lem4  17059  2503lem1  17062  2503lem2  17063  2503lem3  17064  4001lem1  17066  4001lem2  17067  4001lem3  17068  4001prm  17070  pcoass  24978  minveclem2  25380  uniioombllem5  25542  uniioombl  25544  dveflem  25937  pilem2  26416  sinhalfpilem  26426  sincosq1lem  26460  tangtx  26468  sincos4thpi  26476  heron  26802  quad2  26803  dquartlem1  26815  dquart  26817  quart1  26820  atan1  26892  log2ublem3  26912  log2ub  26913  chtub  27177  bclbnd  27245  bpos1  27248  bposlem2  27250  bposlem6  27254  bposlem9  27257  gausslemma2dlem3  27333  m1lgs  27353  2lgslem1a2  27355  2lgslem3a  27361  2lgslem3b  27362  2lgslem3c  27363  2lgslem3d  27364  pntibndlem2  27556  pntlemg  27563  pntlemr  27567  ex-fl  30471  minvecolem2  30899  polid2i  31181  binom2subadd  32770  quad3d  32778  quad3  35813  420lcm8e840  42204  3exp7  42246  3lexlogpow5ineq1  42247  3lexlogpow2ineq2  42252  3lexlogpow5ineq5  42253  aks4d1p1p2  42263  aks4d1p1  42269  2ap1caineq  42338  cxpi11d  42540  flt4lem  42830  3cubeslem3l  42870  3cubeslem3r  42871  wallispi2lem1  46257  wallispi2lem2  46258  stirlinglem3  46262  stirlinglem10  46269  2ltceilhalf  47516  ceil5half3  47528  modmkpkne  47549  fmtnorec4  47737  2exp340mod341  47921  8exp8mod9  47924  ackval2012  48879