Theorem 2t2e4 12427

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 12338	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12401	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12398	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2762	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1536  (class class class)co 7430   + caddc 11155   · cmul 11157  2c2 12318  4c4 12320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-mulcl 11214  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-1rid 11222  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-2 12326  df-3 12327  df-4 12328

This theorem is referenced by:  4d2e2  12433  halfpm6th  12484  div4p1lem1div2  12518  3halfnz  12694  decbin0  12870  fldiv4lem1div2uz2  13872  sq2  14232  sq4e2t8  14234  discr  14275  sqoddm1div8  14278  faclbnd2  14326  4bc2eq6  14364  amgm2  15404  bpoly3  16090  sin4lt0  16227  z4even  16405  flodddiv4  16448  flodddiv4t2lthalf  16451  4nprm  16728  2exp4  17118  2exp16  17124  5prm  17142  631prm  17160  1259lem1  17164  1259lem4  17167  2503lem1  17170  2503lem2  17171  2503lem3  17172  4001lem1  17174  4001lem2  17175  4001lem3  17176  4001prm  17178  pcoass  25070  minveclem2  25473  uniioombllem5  25635  uniioombl  25637  dveflem  26031  pilem2  26510  sinhalfpilem  26519  sincosq1lem  26553  tangtx  26561  sincos4thpi  26569  heron  26895  quad2  26896  dquartlem1  26908  dquart  26910  quart1  26913  atan1  26985  log2ublem3  27005  log2ub  27006  chtub  27270  bclbnd  27338  bpos1  27341  bposlem2  27343  bposlem6  27347  bposlem9  27350  gausslemma2dlem3  27426  m1lgs  27446  2lgslem1a2  27448  2lgslem3a  27454  2lgslem3b  27455  2lgslem3c  27456  2lgslem3d  27457  pntibndlem2  27649  pntlemg  27656  pntlemr  27660  ex-fl  30475  minvecolem2  30903  polid2i  31185  quad3d  32760  quad3  35654  420lcm8e840  41992  3exp7  42034  3lexlogpow5ineq1  42035  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1p1p2  42051  aks4d1p1  42057  2ap1caineq  42126  cxpi11d  42357  flt4lem  42631  3cubeslem3l  42673  3cubeslem3r  42674  wallispi2lem1  46026  wallispi2lem2  46027  stirlinglem3  46031  stirlinglem10  46038  ceil5half3  47279  fmtnorec4  47473  2exp340mod341  47657  8exp8mod9  47660  2ltceilhalf  47949  ackval2012  48540