Theorem 2t2e4 12546

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 12458	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12520	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12517	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2786	1 ⊢ (2 · 2) = 4

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7451   + caddc 11242   · cmul 11244  2c2 12437  4c4 12439

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-mulcl 11301  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-1rid 11309  ax-cnre 11312

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-2 12445  df-3 12446  df-4 12447

This theorem is used by:  4div2e2  12554  div4p1lem1div2  12641  3halfnz  12818  decbin0  13001  fldiv4lem1div2uz2  14016  sq2  14380  sq4e2t8  14382  exp4sqsq  14384  discr  14425  sqoddm1div8  14428  faclbnd2  14476  4bc2eq6  14514  amgm2  15581  bpoly3  16268  sin4lt0  16407  z4even  16586  flodddiv4  16629  flodddiv4t2lthalf  16632  4nprm  16914  2exp4  17306  2exp16  17312  5prm  17330  631prm  17349  1259lem1  17353  1259lem4  17356  2503lem1  17359  2503lem2  17360  2503lem3  17361  4001lem1  17363  4001lem2  17364  4001lem3  17365  4001prm  17367  pcoass  25400  minveclem2  25802  uniioombllem5  25963  uniioombl  25965  dveflem  26354  pilem2  26836  sinhalfpilem  26849  sincosq1lem  26883  tangtx  26891  sincos4thpi  26899  heron  27223  quad2  27224  dquartlem1  27236  dquart  27238  quart1  27241  atan1  27313  log2ublem3  27333  log2ub  27334  chtub  27596  bclbnd  27664  bpos1  27667  bposlem2  27669  bposlem6  27673  bposlem9  27676  gausslemma2dlem3  27752  m1lgs  27772  2lgslem1a2  27774  2lgslem3a  27780  2lgslem3b  27781  2lgslem3c  27782  2lgslem3d  27783  pntibndlem2  27975  pntlemg  27982  pntlemr  27986  ex-fl  31105  minvecolem2  31534  polid2i  31816  binom2subadd  33429  quad3d  33437  quad3  36643  420lcm8e840  43327  3exp7  43369  3lexlogpow5ineq1  43370  3lexlogpow2ineq2  43375  3lexlogpow5ineq5  43376  aks4d1p1p2  43386  aks4d1p1  43392  2ap1caineq  43461  25or6to4  43522  cxpi11d  43660  3cubeslem3l  43962  3cubeslem3r  43963  wallispi2lem1  47354  wallispi2lem2  47355  stirlinglem3  47359  stirlinglem10  47366  sin5tlem2  48193  cos5t  48198  goldpolyfactor  48200  2ltceilhalf  48675  ceil5half3  48689  modmkpkne  48710  fmtnorec4  48907  nprmdvdsfacm1lem4  48981  ppivalnn4  48985  2exp340mod341  49104  8exp8mod9  49107  bru4  49752  bru3val  49753  ackval2012  50134