Theorem 2t2e4 12513

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 12425	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12487	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12484	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2783	1 ⊢ (2 · 2) = 4

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7424   + caddc 11210   · cmul 11212  2c2 12404  4c4 12406

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-resscn 11264  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-mulcl 11269  ax-mulcom 11271  ax-addass 11272  ax-mulass 11273  ax-distr 11274  ax-1rid 11277  ax-cnre 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427  df-2 12412  df-3 12413  df-4 12414

This theorem is used by:  4div2e2  12521  div4p1lem1div2  12608  3halfnz  12785  decbin0  12968  fldiv4lem1div2uz2  13983  sq2  14347  sq4e2t8  14349  exp4sqsq  14351  discr  14391  sqoddm1div8  14394  faclbnd2  14442  4bc2eq6  14480  amgm2  15546  bpoly3  16233  sin4lt0  16372  z4even  16551  flodddiv4  16594  flodddiv4t2lthalf  16597  4nprm  16879  2exp4  17271  2exp16  17277  5prm  17295  631prm  17314  1259lem1  17318  1259lem4  17321  2503lem1  17324  2503lem2  17325  2503lem3  17326  4001lem1  17328  4001lem2  17329  4001lem3  17330  4001prm  17332  pcoass  25354  minveclem2  25756  uniioombllem5  25917  uniioombl  25919  dveflem  26308  pilem2  26788  sinhalfpilem  26801  sincosq1lem  26835  tangtx  26843  sincos4thpi  26851  heron  27175  quad2  27176  dquartlem1  27188  dquart  27190  quart1  27193  atan1  27265  log2ublem3  27285  log2ub  27286  chtub  27548  bclbnd  27616  bpos1  27619  bposlem2  27621  bposlem6  27625  bposlem9  27628  gausslemma2dlem3  27704  m1lgs  27724  2lgslem1a2  27726  2lgslem3a  27732  2lgslem3b  27733  2lgslem3c  27734  2lgslem3d  27735  pntibndlem2  27927  pntlemg  27934  pntlemr  27938  ex-fl  31057  minvecolem2  31486  polid2i  31768  binom2subadd  33383  quad3d  33391  quad3  36553  420lcm8e840  43198  3exp7  43240  3lexlogpow5ineq1  43241  3lexlogpow2ineq2  43246  3lexlogpow5ineq5  43247  aks4d1p1p2  43257  aks4d1p1  43263  2ap1caineq  43332  25or6to4  43393  cxpi11d  43531  3cubeslem3l  43833  3cubeslem3r  43834  wallispi2lem1  47217  wallispi2lem2  47218  stirlinglem3  47222  stirlinglem10  47229  sin5tlem2  48056  cos5t  48061  goldpolyfactor  48063  2ltceilhalf  48538  ceil5half3  48552  modmkpkne  48573  fmtnorec4  48770  nprmdvdsfacm1lem4  48844  ppivalnn4  48848  2exp340mod341  48967  8exp8mod9  48970  ackval2012  49939