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

Theorem 2t2e4 10697
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 10618 . . 3  |-  2  e.  CC
212timesi 10668 . 2  |-  ( 2  x.  2 )  =  ( 2  +  2 )
3 2p2e4 10665 . 2  |-  ( 2  +  2 )  =  4
42, 3eqtri 2496 1  |-  ( 2  x.  2 )  =  4
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379  (class class class)co 6295    + caddc 9507    x. cmul 9509   2c2 10597   4c4 10599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rrecex 9576  ax-cnre 9577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-iota 5557  df-fv 5602  df-ov 6298  df-2 10606  df-3 10607  df-4 10608
This theorem is referenced by:  4d2e2  10704  halfpm6th  10772  decbin0  11091  sq2  12244  discr  12283  faclbnd2  12349  amgm2  13182  sin4lt0  13808  2exp4  14447  2exp6  14448  2exp16  14450  4nprm  14465  5prm  14469  631prm  14487  1259lem1  14488  1259lem4  14491  2503lem1  14494  2503lem2  14495  2503lem3  14496  4001lem1  14498  4001lem2  14499  4001lem3  14500  4001prm  14502  pcoass  21392  minveclem2  21709  uniioombllem5  21864  uniioombl  21866  dveflem  22248  pilem2  22714  sinhalfpilem  22722  sincosq1lem  22756  tangtx  22764  sincos4thpi  22772  heron  23035  quad2  23036  dquartlem1  23048  dquart  23050  quart1  23053  atan1  23125  log2ublem3  23145  log2ub  23146  ppiublem2  23344  chtub  23353  bclbnd  23421  bpos1  23424  bposlem2  23426  bposlem6  23430  bposlem9  23433  m1lgs  23503  pntibndlem2  23642  pntlemg  23649  pntlemr  23653  ex-fl  24992  minvecolem2  25614  polid2i  25897  quad3  28849  4bc2eq6  28937  bpoly3  29747  wallispi2lem1  31694  wallispi2lem2  31695  stirlinglem3  31699  stirlinglem10  31706
  Copyright terms: Public domain W3C validator