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

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

Proof of Theorem 2t2e4
StepHypRef Expression
1 2cn 10602 . . 3  |-  2  e.  CC
212timesi 10652 . 2  |-  ( 2  x.  2 )  =  ( 2  +  2 )
3 2p2e4 10649 . 2  |-  ( 2  +  2 )  =  4
42, 3eqtri 2483 1  |-  ( 2  x.  2 )  =  4
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398  (class class class)co 6270    + caddc 9484    x. cmul 9486   2c2 10581   4c4 10583
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rrecex 9553  ax-cnre 9554
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273  df-2 10590  df-3 10591  df-4 10592
This theorem is referenced by:  4d2e2  10688  halfpm6th  10756  decbin0  11079  sq2  12246  discr  12285  faclbnd2  12351  amgm2  13284  sin4lt0  14012  2exp4  14655  2exp6OLD  14657  2exp16  14659  4nprm  14674  5prm  14678  631prm  14696  1259lem1  14697  1259lem4  14700  2503lem1  14703  2503lem2  14704  2503lem3  14705  4001lem1  14707  4001lem2  14708  4001lem3  14709  4001prm  14711  pcoass  21690  minveclem2  22007  uniioombllem5  22162  uniioombl  22164  dveflem  22546  pilem2  23013  sinhalfpilem  23022  sincosq1lem  23056  tangtx  23064  sincos4thpi  23072  heron  23366  quad2  23367  dquartlem1  23379  dquart  23381  quart1  23384  atan1  23456  log2ublem3  23476  log2ub  23477  ppiublem2  23676  chtub  23685  bclbnd  23753  bpos1  23756  bposlem2  23758  bposlem6  23762  bposlem9  23765  m1lgs  23835  pntibndlem2  23974  pntlemg  23981  pntlemr  23985  ex-fl  25370  minvecolem2  25989  polid2i  26272  quad3  29288  4bc2eq6  29353  bpoly3  30048  wallispi2lem1  32092  wallispi2lem2  32093  stirlinglem3  32097  stirlinglem10  32104  3halfnz  33380
  Copyright terms: Public domain W3C validator