Theorem 2t2e4 12146

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 12057	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12120	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12117	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2767	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1539  (class class class)co 7284   + caddc 10883   · cmul 10885  2c2 12037  4c4 12039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-mulcl 10942  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-1rid 10950  ax-cnre 10953

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287  df-2 12045  df-3 12046  df-4 12047

This theorem is referenced by:  4d2e2  12152  halfpm6th  12203  div4p1lem1div2  12237  3halfnz  12408  decbin0  12586  fldiv4lem1div2uz2  13565  sq2  13923  sq4e2t8  13925  discr  13964  sqoddm1div8  13967  faclbnd2  14014  4bc2eq6  14052  amgm2  15090  bpoly3  15777  sin4lt0  15913  z4even  16090  flodddiv4  16131  flodddiv4t2lthalf  16134  4nprm  16409  2exp4  16795  2exp16  16801  5prm  16819  631prm  16837  1259lem1  16841  1259lem4  16844  2503lem1  16847  2503lem2  16848  2503lem3  16849  4001lem1  16851  4001lem2  16852  4001lem3  16853  4001prm  16855  pcoass  24196  minveclem2  24599  uniioombllem5  24760  uniioombl  24762  dveflem  25152  pilem2  25620  sinhalfpilem  25629  sincosq1lem  25663  tangtx  25671  sincos4thpi  25679  heron  25997  quad2  25998  dquartlem1  26010  dquart  26012  quart1  26015  atan1  26087  log2ublem3  26107  log2ub  26108  chtub  26369  bclbnd  26437  bpos1  26440  bposlem2  26442  bposlem6  26446  bposlem9  26449  gausslemma2dlem3  26525  m1lgs  26545  2lgslem1a2  26547  2lgslem3a  26553  2lgslem3b  26554  2lgslem3c  26555  2lgslem3d  26556  pntibndlem2  26748  pntlemg  26755  pntlemr  26759  ex-fl  28820  minvecolem2  29246  polid2i  29528  quad3  33637  420lcm8e840  40026  3exp7  40068  3lexlogpow5ineq1  40069  3lexlogpow2ineq2  40074  3lexlogpow5ineq5  40075  aks4d1p1p2  40085  aks4d1p1  40091  2ap1caineq  40108  flt4lem  40489  3cubeslem3l  40515  3cubeslem3r  40516  wallispi2lem1  43619  wallispi2lem2  43620  stirlinglem3  43624  stirlinglem10  43631  fmtnorec4  45012  2exp340mod341  45196  8exp8mod9  45199  ackval2012  46048