Theorem 2t2e4 12287

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

Syntax hints:   = wceq 1540  (class class class)co 7349   + caddc 11012   · cmul 11014  2c2 12183  4c4 12185

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 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-mulcl 11071  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-1rid 11079  ax-cnre 11082

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-2 12191  df-3 12192  df-4 12193

This theorem is referenced by:  4d2e2  12293  div4p1lem1div2  12379  3halfnz  12555  decbin0  12731  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  24922  minveclem2  25324  uniioombllem5  25486  uniioombl  25488  dveflem  25881  pilem2  26360  sinhalfpilem  26370  sincosq1lem  26404  tangtx  26412  sincos4thpi  26420  heron  26746  quad2  26747  dquartlem1  26759  dquart  26761  quart1  26764  atan1  26836  log2ublem3  26856  log2ub  26857  chtub  27121  bclbnd  27189  bpos1  27192  bposlem2  27194  bposlem6  27198  bposlem9  27201  gausslemma2dlem3  27277  m1lgs  27297  2lgslem1a2  27299  2lgslem3a  27305  2lgslem3b  27306  2lgslem3c  27307  2lgslem3d  27308  pntibndlem2  27500  pntlemg  27507  pntlemr  27511  ex-fl  30391  minvecolem2  30819  polid2i  31101  binom2subadd  32685  quad3d  32693  quad3  35647  420lcm8e840  41988  3exp7  42030  3lexlogpow5ineq1  42031  3lexlogpow2ineq2  42036  3lexlogpow5ineq5  42037  aks4d1p1p2  42047  aks4d1p1  42053  2ap1caineq  42122  cxpi11d  42320  flt4lem  42622  3cubeslem3l  42663  3cubeslem3r  42664  wallispi2lem1  46056  wallispi2lem2  46057  stirlinglem3  46061  stirlinglem10  46068  2ltceilhalf  47316  ceil5half3  47328  modmkpkne  47349  fmtnorec4  47537  2exp340mod341  47721  8exp8mod9  47724  ackval2012  48680