Theorem 2t2e4 11484

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 11388	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 11458	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 11455	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2821	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1653  (class class class)co 6878   + caddc 10227   · cmul 10229  2c2 11368  4c4 11370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-mulcl 10286  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-1rid 10294  ax-cnre 10297

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-iota 6064  df-fv 6109  df-ov 6881  df-2 11376  df-3 11377  df-4 11378

This theorem is referenced by:  4d2e2  11490  halfpm6th  11541  div4p1lem1div2  11575  3halfnz  11746  decbin0  11925  fldiv4lem1div2uz2  12892  sq2  13214  sq4e2t8  13216  discr  13255  sqoddm1div8  13284  faclbnd2  13331  4bc2eq6  13369  amgm2  14450  bpoly3  15125  sin4lt0  15261  z4even  15444  flodddiv4  15472  flodddiv4t2lthalf  15475  4nprm  15741  2exp4  16122  2exp16  16125  5prm  16143  631prm  16161  1259lem1  16165  1259lem4  16168  2503lem1  16171  2503lem2  16172  2503lem3  16173  4001lem1  16175  4001lem2  16176  4001lem3  16177  4001prm  16179  pcoass  23151  minveclem2  23536  uniioombllem5  23695  uniioombl  23697  dveflem  24083  pilem2  24547  sinhalfpilem  24557  sincosq1lem  24591  tangtx  24599  sincos4thpi  24607  heron  24917  quad2  24918  dquartlem1  24930  dquart  24932  quart1  24935  atan1  25007  log2ublem3  25027  log2ub  25028  ppiublem2  25280  chtub  25289  bclbnd  25357  bpos1  25360  bposlem2  25362  bposlem6  25366  bposlem9  25369  gausslemma2dlem3  25445  m1lgs  25465  2lgslem1a2  25467  2lgslem3a  25473  2lgslem3b  25474  2lgslem3c  25475  2lgslem3d  25476  pntibndlem2  25632  pntlemg  25639  pntlemr  25643  ex-fl  27832  minvecolem2  28256  polid2i  28539  quad3  32079  wallispi2lem1  41031  wallispi2lem2  41032  stirlinglem3  41036  stirlinglem10  41043  fmtnorec4  42243