Theorem 2t2e4 12399

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 12311	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12373	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12370	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2786	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1570  (class class class)co 7410   + caddc 11098   · cmul 11100  2c2 12290  4c4 12292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-mulcl 11157  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-1rid 11165  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-2 12298  df-3 12299  df-4 12300

This theorem is referenced by:  4div2e2  12407  div4p1lem1div2  12494  3halfnz  12670  decbin0  12853  fldiv4lem1div2uz2  13865  sq2  14229  sq4e2t8  14231  discr  14272  sqoddm1div8  14275  faclbnd2  14323  4bc2eq6  14361  amgm2  15417  bpoly3  16107  sin4lt0  16246  z4even  16425  flodddiv4  16468  flodddiv4t2lthalf  16471  4nprm  16748  2exp4  17139  2exp16  17145  5prm  17163  631prm  17182  1259lem1  17186  1259lem4  17189  2503lem1  17192  2503lem2  17193  2503lem3  17194  4001lem1  17196  4001lem2  17197  4001lem3  17198  4001prm  17200  pcoass  25183  minveclem2  25585  uniioombllem5  25746  uniioombl  25748  dveflem  26138  pilem2  26615  sinhalfpilem  26628  sincosq1lem  26662  tangtx  26670  sincos4thpi  26678  heron  27003  quad2  27004  dquartlem1  27016  dquart  27018  quart1  27021  atan1  27093  log2ublem3  27113  log2ub  27114  chtub  27376  bclbnd  27444  bpos1  27447  bposlem2  27449  bposlem6  27453  bposlem9  27456  gausslemma2dlem3  27532  m1lgs  27552  2lgslem1a2  27554  2lgslem3a  27560  2lgslem3b  27561  2lgslem3c  27562  2lgslem3d  27563  pntibndlem2  27755  pntlemg  27762  pntlemr  27766  ex-fl  30798  minvecolem2  31227  polid2i  31509  binom2subadd  33086  quad3d  33094  quad3  36162  420lcm8e840  42778  3exp7  42820  3lexlogpow5ineq1  42821  3lexlogpow2ineq2  42826  3lexlogpow5ineq5  42827  aks4d1p1p2  42837  aks4d1p1  42843  2ap1caineq  42912  25or6to4  42973  cxpi11d  43104  flt4lem  43377  3cubeslem3l  43417  3cubeslem3r  43418  wallispi2lem1  46785  wallispi2lem2  46786  stirlinglem3  46790  stirlinglem10  46797  sin5tlem2  47611  cos5t  47616  2ltceilhalf  48069  ceil5half3  48083  modmkpkne  48104  fmtnorec4  48301  nprmdvdsfacm1lem4  48375  ppivalnn4  48379  2exp340mod341  48498  8exp8mod9  48501  ackval2012  49471