Theorem 2t2e4 12331

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 12247	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12305	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12302	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2762	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1547  (class class class)co 7356   + caddc 11032   · cmul 11034  2c2 12227  4c4 12229

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-1rid 11099  ax-cnre 11102

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359  df-2 12235  df-3 12236  df-4 12237

This theorem is referenced by:  4div2e2  12337  div4p1lem1div2  12423  3halfnz  12599  decbin0  12775  fldiv4lem1div2uz2  13786  sq2  14150  sq4e2t8  14152  discr  14193  sqoddm1div8  14196  faclbnd2  14244  4bc2eq6  14282  amgm2  15323  bpoly3  16014  sin4lt0  16153  z4even  16332  flodddiv4  16375  flodddiv4t2lthalf  16378  4nprm  16655  2exp4  17046  2exp16  17052  5prm  17070  631prm  17088  1259lem1  17092  1259lem4  17095  2503lem1  17098  2503lem2  17099  2503lem3  17100  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001prm  17106  pcoass  25009  minveclem2  25411  uniioombllem5  25572  uniioombl  25574  dveflem  25964  pilem2  26435  sinhalfpilem  26445  sincosq1lem  26479  tangtx  26487  sincos4thpi  26495  heron  26820  quad2  26821  dquartlem1  26833  dquart  26835  quart1  26838  atan1  26910  log2ublem3  26930  log2ub  26931  chtub  27193  bclbnd  27261  bpos1  27264  bposlem2  27266  bposlem6  27270  bposlem9  27273  gausslemma2dlem3  27349  m1lgs  27369  2lgslem1a2  27371  2lgslem3a  27377  2lgslem3b  27378  2lgslem3c  27379  2lgslem3d  27380  pntibndlem2  27572  pntlemg  27579  pntlemr  27583  ex-fl  30535  minvecolem2  30964  polid2i  31246  binom2subadd  32833  quad3d  32841  quad3  35898  420lcm8e840  42496  3exp7  42538  3lexlogpow5ineq1  42539  3lexlogpow2ineq2  42544  3lexlogpow5ineq5  42545  aks4d1p1p2  42555  aks4d1p1  42561  2ap1caineq  42630  cxpi11d  42820  flt4lem  43095  3cubeslem3l  43135  3cubeslem3r  43136  wallispi2lem1  46514  wallispi2lem2  46515  stirlinglem3  46519  stirlinglem10  46526  sin5tlem2  47337  cos5t  47342  2ltceilhalf  47795  ceil5half3  47809  modmkpkne  47830  fmtnorec4  48027  nprmdvdsfacm1lem4  48101  ppivalnn4  48105  2exp340mod341  48224  8exp8mod9  48227  ackval2012  49182