Theorem 2t2e4 12376

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 12287	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12350	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12347	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2761	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1542  (class class class)co 7409   + caddc 11113   · cmul 11115  2c2 12267  4c4 12269

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 2704  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-mulcl 11172  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-1rid 11180  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-2 12275  df-3 12276  df-4 12277

This theorem is referenced by:  4d2e2  12382  halfpm6th  12433  div4p1lem1div2  12467  3halfnz  12641  decbin0  12817  fldiv4lem1div2uz2  13801  sq2  14161  sq4e2t8  14163  discr  14203  sqoddm1div8  14206  faclbnd2  14251  4bc2eq6  14289  amgm2  15316  bpoly3  16002  sin4lt0  16138  z4even  16315  flodddiv4  16356  flodddiv4t2lthalf  16359  4nprm  16632  2exp4  17018  2exp16  17024  5prm  17042  631prm  17060  1259lem1  17064  1259lem4  17067  2503lem1  17070  2503lem2  17071  2503lem3  17072  4001lem1  17074  4001lem2  17075  4001lem3  17076  4001prm  17078  pcoass  24540  minveclem2  24943  uniioombllem5  25104  uniioombl  25106  dveflem  25496  pilem2  25964  sinhalfpilem  25973  sincosq1lem  26007  tangtx  26015  sincos4thpi  26023  heron  26343  quad2  26344  dquartlem1  26356  dquart  26358  quart1  26361  atan1  26433  log2ublem3  26453  log2ub  26454  chtub  26715  bclbnd  26783  bpos1  26786  bposlem2  26788  bposlem6  26792  bposlem9  26795  gausslemma2dlem3  26871  m1lgs  26891  2lgslem1a2  26893  2lgslem3a  26899  2lgslem3b  26900  2lgslem3c  26901  2lgslem3d  26902  pntibndlem2  27094  pntlemg  27101  pntlemr  27105  ex-fl  29700  minvecolem2  30128  polid2i  30410  quad3  34655  420lcm8e840  40876  3exp7  40918  3lexlogpow5ineq1  40919  3lexlogpow2ineq2  40924  3lexlogpow5ineq5  40925  aks4d1p1p2  40935  aks4d1p1  40941  2ap1caineq  40961  flt4lem  41387  3cubeslem3l  41424  3cubeslem3r  41425  wallispi2lem1  44787  wallispi2lem2  44788  stirlinglem3  44792  stirlinglem10  44799  fmtnorec4  46217  2exp340mod341  46401  8exp8mod9  46404  ackval2012  47377