Theorem 2t2e4 12381

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 12293	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12355	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12352	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2785	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1560  (class class class)co 7396   + caddc 11076   · cmul 11078  2c2 12272  4c4 12274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-mulcl 11135  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-1rid 11143  ax-cnre 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-2 12280  df-3 12281  df-4 12282

This theorem is referenced by:  4div2e2  12389  div4p1lem1div2  12476  3halfnz  12652  decbin0  12835  fldiv4lem1div2uz2  13846  sq2  14210  sq4e2t8  14212  discr  14253  sqoddm1div8  14256  faclbnd2  14304  4bc2eq6  14342  amgm2  15397  bpoly3  16088  sin4lt0  16227  z4even  16406  flodddiv4  16449  flodddiv4t2lthalf  16452  4nprm  16729  2exp4  17120  2exp16  17126  5prm  17144  631prm  17163  1259lem1  17167  1259lem4  17170  2503lem1  17173  2503lem2  17174  2503lem3  17175  4001lem1  17177  4001lem2  17178  4001lem3  17179  4001prm  17181  pcoass  25086  minveclem2  25488  uniioombllem5  25649  uniioombl  25651  dveflem  26041  pilem2  26515  sinhalfpilem  26528  sincosq1lem  26562  tangtx  26570  sincos4thpi  26578  heron  26903  quad2  26904  dquartlem1  26916  dquart  26918  quart1  26921  atan1  26993  log2ublem3  27013  log2ub  27014  chtub  27276  bclbnd  27344  bpos1  27347  bposlem2  27349  bposlem6  27353  bposlem9  27356  gausslemma2dlem3  27432  m1lgs  27452  2lgslem1a2  27454  2lgslem3a  27460  2lgslem3b  27461  2lgslem3c  27462  2lgslem3d  27463  pntibndlem2  27655  pntlemg  27662  pntlemr  27666  ex-fl  30649  minvecolem2  31078  polid2i  31360  binom2subadd  32943  quad3d  32951  quad3  36020  420lcm8e840  42628  3exp7  42670  3lexlogpow5ineq1  42671  3lexlogpow2ineq2  42676  3lexlogpow5ineq5  42677  aks4d1p1p2  42687  aks4d1p1  42693  2ap1caineq  42762  cxpi11d  42952  flt4lem  43227  3cubeslem3l  43267  3cubeslem3r  43268  wallispi2lem1  46645  wallispi2lem2  46646  stirlinglem3  46650  stirlinglem10  46657  sin5tlem2  47468  cos5t  47473  2ltceilhalf  47926  ceil5half3  47940  modmkpkne  47961  fmtnorec4  48158  nprmdvdsfacm1lem4  48232  ppivalnn4  48236  2exp340mod341  48355  8exp8mod9  48358  ackval2012  49313