Theorem 2t2e4 11804

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 11715	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 11778	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 11775	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2846	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1537  (class class class)co 7158   + caddc 10542   · cmul 10544  2c2 11695  4c4 11697

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-mulcl 10601  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-1rid 10609  ax-cnre 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161  df-2 11703  df-3 11704  df-4 11705

This theorem is referenced by:  4d2e2  11810  halfpm6th  11861  div4p1lem1div2  11895  3halfnz  12064  decbin0  12241  fldiv4lem1div2uz2  13209  sq2  13563  sq4e2t8  13565  discr  13604  sqoddm1div8  13607  faclbnd2  13654  4bc2eq6  13692  amgm2  14731  bpoly3  15414  sin4lt0  15550  z4even  15725  flodddiv4  15766  flodddiv4t2lthalf  15769  4nprm  16041  2exp4  16423  2exp16  16426  5prm  16444  631prm  16462  1259lem1  16466  1259lem4  16469  2503lem1  16472  2503lem2  16473  2503lem3  16474  4001lem1  16476  4001lem2  16477  4001lem3  16478  4001prm  16480  pcoass  23630  minveclem2  24031  uniioombllem5  24190  uniioombl  24192  dveflem  24578  pilem2  25042  sinhalfpilem  25051  sincosq1lem  25085  tangtx  25093  sincos4thpi  25101  heron  25418  quad2  25419  dquartlem1  25431  dquart  25433  quart1  25436  atan1  25508  log2ublem3  25528  log2ub  25529  chtub  25790  bclbnd  25858  bpos1  25861  bposlem2  25863  bposlem6  25867  bposlem9  25870  gausslemma2dlem3  25946  m1lgs  25966  2lgslem1a2  25968  2lgslem3a  25974  2lgslem3b  25975  2lgslem3c  25976  2lgslem3d  25977  pntibndlem2  26169  pntlemg  26176  pntlemr  26180  ex-fl  28228  minvecolem2  28654  polid2i  28936  quad3  32915  3cubeslem3l  39290  3cubeslem3r  39291  wallispi2lem1  42363  wallispi2lem2  42364  stirlinglem3  42368  stirlinglem10  42375  fmtnorec4  43718  2exp340mod341  43905  8exp8mod9  43908