Theorem 2t2e4 11379

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 11293	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 11349	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 11346	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2793	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1631  (class class class)co 6793   + caddc 10141   · cmul 10143  2c2 11272  4c4 11274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rrecex 10210  ax-cnre 10211

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5994  df-fv 6039  df-ov 6796  df-2 11281  df-3 11282  df-4 11283

This theorem is referenced by:  4d2e2  11386  halfpm6th  11455  div4p1lem1div2  11489  3halfnz  11658  decbin0  11883  fldiv4lem1div2uz2  12845  sq2  13167  sq4e2t8  13169  discr  13208  sqoddm1div8  13235  faclbnd2  13282  4bc2eq6  13320  amgm2  14317  bpoly3  14995  sin4lt0  15131  z4even  15316  flodddiv4  15345  flodddiv4t2lthalf  15348  4nprm  15614  2exp4  16001  2exp16  16004  5prm  16022  631prm  16041  1259lem1  16045  1259lem4  16048  2503lem1  16051  2503lem2  16052  2503lem3  16053  4001lem1  16055  4001lem2  16056  4001lem3  16057  4001prm  16059  pcoass  23043  minveclem2  23416  uniioombllem5  23575  uniioombl  23577  dveflem  23962  pilem2  24426  sinhalfpilem  24436  sincosq1lem  24470  tangtx  24478  sincos4thpi  24486  heron  24786  quad2  24787  dquartlem1  24799  dquart  24801  quart1  24804  atan1  24876  log2ublem3  24896  log2ub  24897  ppiublem2  25149  chtub  25158  bclbnd  25226  bpos1  25229  bposlem2  25231  bposlem6  25235  bposlem9  25238  gausslemma2dlem3  25314  m1lgs  25334  2lgslem1a2  25336  2lgslem3a  25342  2lgslem3b  25343  2lgslem3c  25344  2lgslem3d  25345  pntibndlem2  25501  pntlemg  25508  pntlemr  25512  ex-fl  27646  minvecolem2  28071  polid2i  28354  quad3  31902  wallispi2lem1  40805  wallispi2lem2  40806  stirlinglem3  40810  stirlinglem10  40817  fmtnorec4  41989