Theorem 2t2e4 12419

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 12331	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12393	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12390	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2788	1 ⊢ (2 · 2) = 4

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7419   + caddc 11118   · cmul 11120  2c2 12310  4c4 12312

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-resscn 11172  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-mulcl 11177  ax-mulcom 11179  ax-addass 11180  ax-mulass 11181  ax-distr 11182  ax-1rid 11185  ax-cnre 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12318  df-3 12319  df-4 12320

This theorem is used by:  4div2e2  12427  div4p1lem1div2  12514  3halfnz  12691  decbin0  12874  fldiv4lem1div2uz2  13887  sq2  14251  sq4e2t8  14253  discr  14294  sqoddm1div8  14297  faclbnd2  14345  4bc2eq6  14383  amgm2  15445  bpoly3  16134  sin4lt0  16273  z4even  16452  flodddiv4  16495  flodddiv4t2lthalf  16498  4nprm  16775  2exp4  17166  2exp16  17172  5prm  17190  631prm  17209  1259lem1  17213  1259lem4  17216  2503lem1  17219  2503lem2  17220  2503lem3  17221  4001lem1  17223  4001lem2  17224  4001lem3  17225  4001prm  17227  pcoass  25234  minveclem2  25636  uniioombllem5  25797  uniioombl  25799  dveflem  26189  pilem2  26666  sinhalfpilem  26679  sincosq1lem  26713  tangtx  26721  sincos4thpi  26729  heron  27054  quad2  27055  dquartlem1  27067  dquart  27069  quart1  27072  atan1  27144  log2ublem3  27164  log2ub  27165  chtub  27427  bclbnd  27495  bpos1  27498  bposlem2  27500  bposlem6  27504  bposlem9  27507  gausslemma2dlem3  27583  m1lgs  27603  2lgslem1a2  27605  2lgslem3a  27611  2lgslem3b  27612  2lgslem3c  27613  2lgslem3d  27614  pntibndlem2  27806  pntlemg  27813  pntlemr  27817  ex-fl  30869  minvecolem2  31298  polid2i  31580  binom2subadd  33156  quad3d  33164  quad3  36199  420lcm8e840  42836  3exp7  42878  3lexlogpow5ineq1  42879  3lexlogpow2ineq2  42884  3lexlogpow5ineq5  42885  aks4d1p1p2  42895  aks4d1p1  42901  2ap1caineq  42970  25or6to4  43031  cxpi11d  43162  flt4lem  43435  3cubeslem3l  43475  3cubeslem3r  43476  wallispi2lem1  46843  wallispi2lem2  46844  stirlinglem3  46848  stirlinglem10  46855  sin5tlem2  47669  cos5t  47674  2ltceilhalf  48127  ceil5half3  48141  modmkpkne  48162  fmtnorec4  48359  nprmdvdsfacm1lem4  48433  ppivalnn4  48437  2exp340mod341  48556  8exp8mod9  48559  ackval2012  49528