Theorem 2t2e4 12352

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 12268	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12326	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12323	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2753	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1540  (class class class)co 7390   + caddc 11078   · cmul 11080  2c2 12248  4c4 12250

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 2702  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-1rid 11145  ax-cnre 11148

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 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-2 12256  df-3 12257  df-4 12258

This theorem is referenced by:  4d2e2  12358  div4p1lem1div2  12444  3halfnz  12620  decbin0  12796  fldiv4lem1div2uz2  13805  sq2  14169  sq4e2t8  14171  discr  14212  sqoddm1div8  14215  faclbnd2  14263  4bc2eq6  14301  amgm2  15343  bpoly3  16031  sin4lt0  16170  z4even  16349  flodddiv4  16392  flodddiv4t2lthalf  16395  4nprm  16672  2exp4  17062  2exp16  17068  5prm  17086  631prm  17104  1259lem1  17108  1259lem4  17111  2503lem1  17114  2503lem2  17115  2503lem3  17116  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001prm  17122  pcoass  24931  minveclem2  25333  uniioombllem5  25495  uniioombl  25497  dveflem  25890  pilem2  26369  sinhalfpilem  26379  sincosq1lem  26413  tangtx  26421  sincos4thpi  26429  heron  26755  quad2  26756  dquartlem1  26768  dquart  26770  quart1  26773  atan1  26845  log2ublem3  26865  log2ub  26866  chtub  27130  bclbnd  27198  bpos1  27201  bposlem2  27203  bposlem6  27207  bposlem9  27210  gausslemma2dlem3  27286  m1lgs  27306  2lgslem1a2  27308  2lgslem3a  27314  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  pntibndlem2  27509  pntlemg  27516  pntlemr  27520  ex-fl  30383  minvecolem2  30811  polid2i  31093  binom2subadd  32672  quad3d  32680  quad3  35664  420lcm8e840  42006  3exp7  42048  3lexlogpow5ineq1  42049  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  aks4d1p1p2  42065  aks4d1p1  42071  2ap1caineq  42140  cxpi11d  42338  flt4lem  42640  3cubeslem3l  42681  3cubeslem3r  42682  wallispi2lem1  46076  wallispi2lem2  46077  stirlinglem3  46081  stirlinglem10  46088  2ltceilhalf  47333  ceil5half3  47345  modmkpkne  47366  fmtnorec4  47554  2exp340mod341  47738  8exp8mod9  47741  ackval2012  48684