Theorem 2t2e4 12326

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 12237	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12300	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12297	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2759	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1541  (class class class)co 7362   + caddc 11063   · cmul 11065  2c2 12217  4c4 12219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-resscn 11117  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-mulcl 11122  ax-mulcom 11124  ax-addass 11125  ax-mulass 11126  ax-distr 11127  ax-1rid 11130  ax-cnre 11133

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-2 12225  df-3 12226  df-4 12227

This theorem is referenced by:  4d2e2  12332  halfpm6th  12383  div4p1lem1div2  12417  3halfnz  12591  decbin0  12767  fldiv4lem1div2uz2  13751  sq2  14111  sq4e2t8  14113  discr  14153  sqoddm1div8  14156  faclbnd2  14201  4bc2eq6  14239  amgm2  15266  bpoly3  15952  sin4lt0  16088  z4even  16265  flodddiv4  16306  flodddiv4t2lthalf  16309  4nprm  16582  2exp4  16968  2exp16  16974  5prm  16992  631prm  17010  1259lem1  17014  1259lem4  17017  2503lem1  17020  2503lem2  17021  2503lem3  17022  4001lem1  17024  4001lem2  17025  4001lem3  17026  4001prm  17028  pcoass  24424  minveclem2  24827  uniioombllem5  24988  uniioombl  24990  dveflem  25380  pilem2  25848  sinhalfpilem  25857  sincosq1lem  25891  tangtx  25899  sincos4thpi  25907  heron  26225  quad2  26226  dquartlem1  26238  dquart  26240  quart1  26243  atan1  26315  log2ublem3  26335  log2ub  26336  chtub  26597  bclbnd  26665  bpos1  26668  bposlem2  26670  bposlem6  26674  bposlem9  26677  gausslemma2dlem3  26753  m1lgs  26773  2lgslem1a2  26775  2lgslem3a  26781  2lgslem3b  26782  2lgslem3c  26783  2lgslem3d  26784  pntibndlem2  26976  pntlemg  26983  pntlemr  26987  ex-fl  29454  minvecolem2  29880  polid2i  30162  quad3  34345  420lcm8e840  40541  3exp7  40583  3lexlogpow5ineq1  40584  3lexlogpow2ineq2  40589  3lexlogpow5ineq5  40590  aks4d1p1p2  40600  aks4d1p1  40606  2ap1caineq  40626  flt4lem  41041  3cubeslem3l  41067  3cubeslem3r  41068  wallispi2lem1  44432  wallispi2lem2  44433  stirlinglem3  44437  stirlinglem10  44444  fmtnorec4  45861  2exp340mod341  46045  8exp8mod9  46048  ackval2012  46897