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  24957  minveclem2  25359  uniioombllem5  25521  uniioombl  25523  dveflem  25916  pilem2  26395  sinhalfpilem  26405  sincosq1lem  26439  tangtx  26447  sincos4thpi  26455  heron  26781  quad2  26782  dquartlem1  26794  dquart  26796  quart1  26799  atan1  26871  log2ublem3  26891  log2ub  26892  chtub  27156  bclbnd  27224  bpos1  27227  bposlem2  27229  bposlem6  27233  bposlem9  27236  gausslemma2dlem3  27312  m1lgs  27332  2lgslem1a2  27334  2lgslem3a  27340  2lgslem3b  27341  2lgslem3c  27342  2lgslem3d  27343  pntibndlem2  27535  pntlemg  27542  pntlemr  27546  ex-fl  30426  minvecolem2  30854  polid2i  31136  binom2subadd  32715  quad3d  32723  quad3  35650  420lcm8e840  41992  3exp7  42034  3lexlogpow5ineq1  42035  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1p1p2  42051  aks4d1p1  42057  2ap1caineq  42126  cxpi11d  42324  flt4lem  42626  3cubeslem3l  42667  3cubeslem3r  42668  wallispi2lem1  46062  wallispi2lem2  46063  stirlinglem3  46067  stirlinglem10  46074  2ltceilhalf  47322  ceil5half3  47334  modmkpkne  47355  fmtnorec4  47543  2exp340mod341  47727  8exp8mod9  47730  ackval2012  48673