Theorem 2t2e4 12403

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 12315	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12377	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12374	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2792	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1567  (class class class)co 7411   + caddc 11102   · cmul 11104  2c2 12294  4c4 12296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-mulcl 11161  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-1rid 11169  ax-cnre 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-2 12302  df-3 12303  df-4 12304

This theorem is referenced by:  4div2e2  12411  div4p1lem1div2  12498  3halfnz  12674  decbin0  12857  fldiv4lem1div2uz2  13868  sq2  14232  sq4e2t8  14234  discr  14275  sqoddm1div8  14278  faclbnd2  14326  4bc2eq6  14364  amgm2  15420  bpoly3  16111  sin4lt0  16250  z4even  16429  flodddiv4  16472  flodddiv4t2lthalf  16475  4nprm  16752  2exp4  17143  2exp16  17149  5prm  17167  631prm  17186  1259lem1  17190  1259lem4  17193  2503lem1  17196  2503lem2  17197  2503lem3  17198  4001lem1  17200  4001lem2  17201  4001lem3  17202  4001prm  17204  pcoass  25151  minveclem2  25553  uniioombllem5  25714  uniioombl  25716  dveflem  26106  pilem2  26580  sinhalfpilem  26593  sincosq1lem  26627  tangtx  26635  sincos4thpi  26643  heron  26968  quad2  26969  dquartlem1  26981  dquart  26983  quart1  26986  atan1  27058  log2ublem3  27078  log2ub  27079  chtub  27341  bclbnd  27409  bpos1  27412  bposlem2  27414  bposlem6  27418  bposlem9  27421  gausslemma2dlem3  27497  m1lgs  27517  2lgslem1a2  27519  2lgslem3a  27525  2lgslem3b  27526  2lgslem3c  27527  2lgslem3d  27528  pntibndlem2  27720  pntlemg  27727  pntlemr  27731  ex-fl  30738  minvecolem2  31167  polid2i  31449  binom2subadd  33026  quad3d  33034  quad3  36060  420lcm8e840  42667  3exp7  42709  3lexlogpow5ineq1  42710  3lexlogpow2ineq2  42715  3lexlogpow5ineq5  42716  aks4d1p1p2  42726  aks4d1p1  42732  2ap1caineq  42801  25or6to4  42862  cxpi11d  42993  flt4lem  43268  3cubeslem3l  43308  3cubeslem3r  43309  wallispi2lem1  46676  wallispi2lem2  46677  stirlinglem3  46681  stirlinglem10  46688  sin5tlem2  47499  cos5t  47504  2ltceilhalf  47957  ceil5half3  47971  modmkpkne  47992  fmtnorec4  48189  nprmdvdsfacm1lem4  48263  ppivalnn4  48267  2exp340mod341  48386  8exp8mod9  48389  ackval2012  49355