Theorem 2t2e4 12506

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 12418	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12480	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12477	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2784	1 ⊢ (2 · 2) = 4

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7420   + caddc 11203   · cmul 11205  2c2 12397  4c4 12399

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 2147  ax-9 2155  ax-ext 2733  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-mulcl 11262  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-1rid 11270  ax-cnre 11273

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 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-2 12405  df-3 12406  df-4 12407

This theorem is used by:  4div2e2  12514  div4p1lem1div2  12601  3halfnz  12778  decbin0  12961  fldiv4lem1div2uz2  13976  sq2  14340  sq4e2t8  14342  exp4sqsq  14344  discr  14384  sqoddm1div8  14387  faclbnd2  14435  4bc2eq6  14473  amgm2  15537  bpoly3  16224  sin4lt0  16363  z4even  16542  flodddiv4  16585  flodddiv4t2lthalf  16588  4nprm  16870  2exp4  17262  2exp16  17268  5prm  17286  631prm  17305  1259lem1  17309  1259lem4  17312  2503lem1  17315  2503lem2  17316  2503lem3  17317  4001lem1  17319  4001lem2  17320  4001lem3  17321  4001prm  17323  pcoass  25345  minveclem2  25747  uniioombllem5  25908  uniioombl  25910  dveflem  26299  pilem2  26779  sinhalfpilem  26792  sincosq1lem  26826  tangtx  26834  sincos4thpi  26842  heron  27166  quad2  27167  dquartlem1  27179  dquart  27181  quart1  27184  atan1  27256  log2ublem3  27276  log2ub  27277  chtub  27539  bclbnd  27607  bpos1  27610  bposlem2  27612  bposlem6  27616  bposlem9  27619  gausslemma2dlem3  27695  m1lgs  27715  2lgslem1a2  27717  2lgslem3a  27723  2lgslem3b  27724  2lgslem3c  27725  2lgslem3d  27726  pntibndlem2  27918  pntlemg  27925  pntlemr  27929  ex-fl  31048  minvecolem2  31477  polid2i  31759  binom2subadd  33333  quad3d  33341  quad3  36435  420lcm8e840  43061  3exp7  43103  3lexlogpow5ineq1  43104  3lexlogpow2ineq2  43109  3lexlogpow5ineq5  43110  aks4d1p1p2  43120  aks4d1p1  43126  2ap1caineq  43195  25or6to4  43256  cxpi11d  43394  3cubeslem3l  43696  3cubeslem3r  43697  wallispi2lem1  47080  wallispi2lem2  47081  stirlinglem3  47085  stirlinglem10  47092  sin5tlem2  47919  cos5t  47924  goldpolyfactor  47926  2ltceilhalf  48401  ceil5half3  48415  modmkpkne  48436  fmtnorec4  48633  nprmdvdsfacm1lem4  48707  ppivalnn4  48711  2exp340mod341  48830  8exp8mod9  48833  ackval2012  49802