Theorem 2t2e4 12404

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 12315	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12378	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12375	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2758	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1540  (class class class)co 7405   + caddc 11132   · cmul 11134  2c2 12295  4c4 12297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-mulcl 11191  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-1rid 11199  ax-cnre 11202

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408  df-2 12303  df-3 12304  df-4 12305

This theorem is referenced by:  4d2e2  12410  div4p1lem1div2  12496  3halfnz  12672  decbin0  12848  fldiv4lem1div2uz2  13853  sq2  14215  sq4e2t8  14217  discr  14258  sqoddm1div8  14261  faclbnd2  14309  4bc2eq6  14347  amgm2  15388  bpoly3  16074  sin4lt0  16213  z4even  16391  flodddiv4  16434  flodddiv4t2lthalf  16437  4nprm  16714  2exp4  17104  2exp16  17110  5prm  17128  631prm  17146  1259lem1  17150  1259lem4  17153  2503lem1  17156  2503lem2  17157  2503lem3  17158  4001lem1  17160  4001lem2  17161  4001lem3  17162  4001prm  17164  pcoass  24975  minveclem2  25378  uniioombllem5  25540  uniioombl  25542  dveflem  25935  pilem2  26414  sinhalfpilem  26424  sincosq1lem  26458  tangtx  26466  sincos4thpi  26474  heron  26800  quad2  26801  dquartlem1  26813  dquart  26815  quart1  26818  atan1  26890  log2ublem3  26910  log2ub  26911  chtub  27175  bclbnd  27243  bpos1  27246  bposlem2  27248  bposlem6  27252  bposlem9  27255  gausslemma2dlem3  27331  m1lgs  27351  2lgslem1a2  27353  2lgslem3a  27359  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  pntibndlem2  27554  pntlemg  27561  pntlemr  27565  ex-fl  30428  minvecolem2  30856  polid2i  31138  binom2subadd  32719  quad3d  32727  quad3  35692  420lcm8e840  42024  3exp7  42066  3lexlogpow5ineq1  42067  3lexlogpow2ineq2  42072  3lexlogpow5ineq5  42073  aks4d1p1p2  42083  aks4d1p1  42089  2ap1caineq  42158  cxpi11d  42392  flt4lem  42668  3cubeslem3l  42709  3cubeslem3r  42710  wallispi2lem1  46100  wallispi2lem2  46101  stirlinglem3  46105  stirlinglem10  46112  2ltceilhalf  47357  ceil5half3  47369  fmtnorec4  47563  2exp340mod341  47747  8exp8mod9  47750  ackval2012  48671