MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2t2e4 Structured version   Visualization version   GIF version

Theorem 2t2e4 11215
Description: 2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.)
Assertion
Ref Expression
2t2e4 (2 · 2) = 4

Proof of Theorem 2t2e4
StepHypRef Expression
1 2cn 11129 . . 3 2 ∈ ℂ
212timesi 11185 . 2 (2 · 2) = (2 + 2)
3 2p2e4 11182 . 2 (2 + 2) = 4
42, 3eqtri 2673 1 (2 · 2) = 4
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  (class class class)co 6690   + caddc 9977   · cmul 9979  2c2 11108  4c4 11110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-2 11117  df-3 11118  df-4 11119
This theorem is referenced by:  4d2e2  11222  halfpm6th  11291  div4p1lem1div2  11325  3halfnz  11494  decbin0  11720  fldiv4lem1div2uz2  12677  sq2  13000  sq4e2t8  13002  discr  13041  sqoddm1div8  13068  faclbnd2  13118  4bc2eq6  13156  amgm2  14153  bpoly3  14833  sin4lt0  14969  z4even  15155  flodddiv4  15184  flodddiv4t2lthalf  15187  4nprm  15454  2exp4  15841  2exp16  15844  5prm  15862  631prm  15881  1259lem1  15885  1259lem4  15888  2503lem1  15891  2503lem2  15892  2503lem3  15893  4001lem1  15895  4001lem2  15896  4001lem3  15897  4001prm  15899  pcoass  22870  minveclem2  23243  uniioombllem5  23401  uniioombl  23403  dveflem  23787  pilem2  24251  sinhalfpilem  24260  sincosq1lem  24294  tangtx  24302  sincos4thpi  24310  heron  24610  quad2  24611  dquartlem1  24623  dquart  24625  quart1  24628  atan1  24700  log2ublem3  24720  log2ub  24721  ppiublem2  24973  chtub  24982  bclbnd  25050  bpos1  25053  bposlem2  25055  bposlem6  25059  bposlem9  25062  gausslemma2dlem3  25138  m1lgs  25158  2lgslem1a2  25160  2lgslem3a  25166  2lgslem3b  25167  2lgslem3c  25168  2lgslem3d  25169  pntibndlem2  25325  pntlemg  25332  pntlemr  25336  ex-fl  27434  minvecolem2  27859  polid2i  28142  quad3  31690  wallispi2lem1  40606  wallispi2lem2  40607  stirlinglem3  40611  stirlinglem10  40618  fmtnorec4  41786
  Copyright terms: Public domain W3C validator