Theorem 2t2e4 12284

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 12200	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12258	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12255	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2754	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1541  (class class class)co 7346   + caddc 11009   · cmul 11011  2c2 12180  4c4 12182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-mulcl 11068  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-1rid 11076  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349  df-2 12188  df-3 12189  df-4 12190

This theorem is referenced by:  4d2e2  12290  div4p1lem1div2  12376  3halfnz  12552  decbin0  12728  fldiv4lem1div2uz2  13740  sq2  14104  sq4e2t8  14106  discr  14147  sqoddm1div8  14150  faclbnd2  14198  4bc2eq6  14236  amgm2  15277  bpoly3  15965  sin4lt0  16104  z4even  16283  flodddiv4  16326  flodddiv4t2lthalf  16329  4nprm  16606  2exp4  16996  2exp16  17002  5prm  17020  631prm  17038  1259lem1  17042  1259lem4  17045  2503lem1  17048  2503lem2  17049  2503lem3  17050  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001prm  17056  pcoass  24951  minveclem2  25353  uniioombllem5  25515  uniioombl  25517  dveflem  25910  pilem2  26389  sinhalfpilem  26399  sincosq1lem  26433  tangtx  26441  sincos4thpi  26449  heron  26775  quad2  26776  dquartlem1  26788  dquart  26790  quart1  26793  atan1  26865  log2ublem3  26885  log2ub  26886  chtub  27150  bclbnd  27218  bpos1  27221  bposlem2  27223  bposlem6  27227  bposlem9  27230  gausslemma2dlem3  27306  m1lgs  27326  2lgslem1a2  27328  2lgslem3a  27334  2lgslem3b  27335  2lgslem3c  27336  2lgslem3d  27337  pntibndlem2  27529  pntlemg  27536  pntlemr  27540  ex-fl  30427  minvecolem2  30855  polid2i  31137  binom2subadd  32725  quad3d  32733  quad3  35714  420lcm8e840  42114  3exp7  42156  3lexlogpow5ineq1  42157  3lexlogpow2ineq2  42162  3lexlogpow5ineq5  42163  aks4d1p1p2  42173  aks4d1p1  42179  2ap1caineq  42248  cxpi11d  42446  flt4lem  42748  3cubeslem3l  42789  3cubeslem3r  42790  wallispi2lem1  46179  wallispi2lem2  46180  stirlinglem3  46184  stirlinglem10  46191  2ltceilhalf  47438  ceil5half3  47450  modmkpkne  47471  fmtnorec4  47659  2exp340mod341  47843  8exp8mod9  47846  ackval2012  48802