Theorem 2t2e4 12408

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7410   + caddc 11107   · cmul 11109  2c2 12299  4c4 12301

This proof depends on 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 11161  ax-1cn 11162  ax-icn 11163  ax-addcl 11164  ax-mulcl 11166  ax-mulcom 11168  ax-addass 11169  ax-mulass 11170  ax-distr 11171  ax-1rid 11174  ax-cnre 11177

This proof 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 12307  df-3 12308  df-4 12309

This theorem is used by:  4div2e2  12416  div4p1lem1div2  12503  3halfnz  12679  decbin0  12862  fldiv4lem1div2uz2  13874  sq2  14238  sq4e2t8  14240  discr  14281  sqoddm1div8  14284  faclbnd2  14332  4bc2eq6  14370  amgm2  15426  bpoly3  16116  sin4lt0  16255  z4even  16434  flodddiv4  16477  flodddiv4t2lthalf  16480  4nprm  16757  2exp4  17148  2exp16  17154  5prm  17172  631prm  17191  1259lem1  17195  1259lem4  17198  2503lem1  17201  2503lem2  17202  2503lem3  17203  4001lem1  17205  4001lem2  17206  4001lem3  17207  4001prm  17209  pcoass  25192  minveclem2  25594  uniioombllem5  25755  uniioombl  25757  dveflem  26147  pilem2  26624  sinhalfpilem  26637  sincosq1lem  26671  tangtx  26679  sincos4thpi  26687  heron  27012  quad2  27013  dquartlem1  27025  dquart  27027  quart1  27030  atan1  27102  log2ublem3  27122  log2ub  27123  chtub  27385  bclbnd  27453  bpos1  27456  bposlem2  27458  bposlem6  27462  bposlem9  27465  gausslemma2dlem3  27541  m1lgs  27561  2lgslem1a2  27563  2lgslem3a  27569  2lgslem3b  27570  2lgslem3c  27571  2lgslem3d  27572  pntibndlem2  27764  pntlemg  27771  pntlemr  27775  ex-fl  30807  minvecolem2  31236  polid2i  31518  binom2subadd  33095  quad3d  33103  quad3  36170  420lcm8e840  42806  3exp7  42848  3lexlogpow5ineq1  42849  3lexlogpow2ineq2  42854  3lexlogpow5ineq5  42855  aks4d1p1p2  42865  aks4d1p1  42871  2ap1caineq  42940  25or6to4  43001  cxpi11d  43132  flt4lem  43405  3cubeslem3l  43445  3cubeslem3r  43446  wallispi2lem1  46813  wallispi2lem2  46814  stirlinglem3  46818  stirlinglem10  46825  sin5tlem2  47639  cos5t  47644  2ltceilhalf  48097  ceil5half3  48111  modmkpkne  48132  fmtnorec4  48329  nprmdvdsfacm1lem4  48403  ppivalnn4  48407  2exp340mod341  48526  8exp8mod9  48529  ackval2012  49499