Theorem 2t2e4 12321

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 12237	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12295	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12292	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2752	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1540  (class class class)co 7369   + caddc 11047   · cmul 11049  2c2 12217  4c4 12219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-mulcl 11106  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-1rid 11114  ax-cnre 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-2 12225  df-3 12226  df-4 12227

This theorem is referenced by:  4d2e2  12327  div4p1lem1div2  12413  3halfnz  12589  decbin0  12765  fldiv4lem1div2uz2  13774  sq2  14138  sq4e2t8  14140  discr  14181  sqoddm1div8  14184  faclbnd2  14232  4bc2eq6  14270  amgm2  15312  bpoly3  16000  sin4lt0  16139  z4even  16318  flodddiv4  16361  flodddiv4t2lthalf  16364  4nprm  16641  2exp4  17031  2exp16  17037  5prm  17055  631prm  17073  1259lem1  17077  1259lem4  17080  2503lem1  17083  2503lem2  17084  2503lem3  17085  4001lem1  17087  4001lem2  17088  4001lem3  17089  4001prm  17091  pcoass  24900  minveclem2  25302  uniioombllem5  25464  uniioombl  25466  dveflem  25859  pilem2  26338  sinhalfpilem  26348  sincosq1lem  26382  tangtx  26390  sincos4thpi  26398  heron  26724  quad2  26725  dquartlem1  26737  dquart  26739  quart1  26742  atan1  26814  log2ublem3  26834  log2ub  26835  chtub  27099  bclbnd  27167  bpos1  27170  bposlem2  27172  bposlem6  27176  bposlem9  27179  gausslemma2dlem3  27255  m1lgs  27275  2lgslem1a2  27277  2lgslem3a  27283  2lgslem3b  27284  2lgslem3c  27285  2lgslem3d  27286  pntibndlem2  27478  pntlemg  27485  pntlemr  27489  ex-fl  30349  minvecolem2  30777  polid2i  31059  binom2subadd  32638  quad3d  32646  quad3  35630  420lcm8e840  41972  3exp7  42014  3lexlogpow5ineq1  42015  3lexlogpow2ineq2  42020  3lexlogpow5ineq5  42021  aks4d1p1p2  42031  aks4d1p1  42037  2ap1caineq  42106  cxpi11d  42304  flt4lem  42606  3cubeslem3l  42647  3cubeslem3r  42648  wallispi2lem1  46042  wallispi2lem2  46043  stirlinglem3  46047  stirlinglem10  46054  2ltceilhalf  47302  ceil5half3  47314  modmkpkne  47335  fmtnorec4  47523  2exp340mod341  47707  8exp8mod9  47710  ackval2012  48653