Theorem 2t2e4 12067

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 11978	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12041	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12038	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2766	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1539  (class class class)co 7255   + caddc 10805   · cmul 10807  2c2 11958  4c4 11960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-mulcl 10864  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-1rid 10872  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-2 11966  df-3 11967  df-4 11968

This theorem is referenced by:  4d2e2  12073  halfpm6th  12124  div4p1lem1div2  12158  3halfnz  12329  decbin0  12506  fldiv4lem1div2uz2  13484  sq2  13842  sq4e2t8  13844  discr  13883  sqoddm1div8  13886  faclbnd2  13933  4bc2eq6  13971  amgm2  15009  bpoly3  15696  sin4lt0  15832  z4even  16009  flodddiv4  16050  flodddiv4t2lthalf  16053  4nprm  16328  2exp4  16714  2exp16  16720  5prm  16738  631prm  16756  1259lem1  16760  1259lem4  16763  2503lem1  16766  2503lem2  16767  2503lem3  16768  4001lem1  16770  4001lem2  16771  4001lem3  16772  4001prm  16774  pcoass  24093  minveclem2  24495  uniioombllem5  24656  uniioombl  24658  dveflem  25048  pilem2  25516  sinhalfpilem  25525  sincosq1lem  25559  tangtx  25567  sincos4thpi  25575  heron  25893  quad2  25894  dquartlem1  25906  dquart  25908  quart1  25911  atan1  25983  log2ublem3  26003  log2ub  26004  chtub  26265  bclbnd  26333  bpos1  26336  bposlem2  26338  bposlem6  26342  bposlem9  26345  gausslemma2dlem3  26421  m1lgs  26441  2lgslem1a2  26443  2lgslem3a  26449  2lgslem3b  26450  2lgslem3c  26451  2lgslem3d  26452  pntibndlem2  26644  pntlemg  26651  pntlemr  26655  ex-fl  28712  minvecolem2  29138  polid2i  29420  quad3  33528  420lcm8e840  39947  3exp7  39989  3lexlogpow5ineq1  39990  3lexlogpow2ineq2  39995  3lexlogpow5ineq5  39996  aks4d1p1p2  40006  aks4d1p1  40012  2ap1caineq  40029  flt4lem  40398  3cubeslem3l  40424  3cubeslem3r  40425  wallispi2lem1  43502  wallispi2lem2  43503  stirlinglem3  43507  stirlinglem10  43514  fmtnorec4  44889  2exp340mod341  45073  8exp8mod9  45076  ackval2012  45925