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

Theorem 2t2e4 10470
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 10391 . . 3  |-  2  e.  CC
212timesi 10441 . 2  |-  ( 2  x.  2 )  =  ( 2  +  2 )
3 2p2e4 10438 . 2  |-  ( 2  +  2 )  =  4
42, 3eqtri 2462 1  |-  ( 2  x.  2 )  =  4
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369  (class class class)co 6090    + caddc 9284    x. cmul 9286   2c2 10370   4c4 10372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-resscn 9338  ax-1cn 9339  ax-icn 9340  ax-addcl 9341  ax-addrcl 9342  ax-mulcl 9343  ax-mulrcl 9344  ax-mulcom 9345  ax-addass 9346  ax-mulass 9347  ax-distr 9348  ax-i2m1 9349  ax-1ne0 9350  ax-1rid 9351  ax-rrecex 9353  ax-cnre 9354
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2719  df-rex 2720  df-rab 2723  df-v 2973  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-nul 3637  df-if 3791  df-sn 3877  df-pr 3879  df-op 3883  df-uni 4091  df-br 4292  df-iota 5380  df-fv 5425  df-ov 6093  df-2 10379  df-3 10380  df-4 10381
This theorem is referenced by:  4d2e2  10477  halfpm6th  10545  decbin0  10857  sq2  11961  discr  12000  faclbnd2  12066  amgm2  12856  sin4lt0  13478  2exp4  14113  2exp6  14114  2exp16  14116  4nprm  14131  5prm  14135  631prm  14153  1259lem1  14154  1259lem4  14157  2503lem1  14160  2503lem2  14161  2503lem3  14162  4001lem1  14164  4001lem2  14165  4001lem3  14166  4001prm  14168  pcoass  20595  minveclem2  20912  uniioombllem5  21066  uniioombl  21068  dveflem  21450  pilem2  21916  sinhalfpilem  21924  sincosq1lem  21958  tangtx  21966  sincos4thpi  21974  heron  22232  quad2  22233  dquartlem1  22245  dquart  22247  quart1  22250  atan1  22322  log2ublem3  22342  log2ub  22343  ppiublem2  22541  chtub  22550  bclbnd  22618  bpos1  22621  bposlem2  22623  bposlem6  22627  bposlem9  22630  m1lgs  22700  pntibndlem2  22839  pntlemg  22846  pntlemr  22850  ex-fl  23653  minvecolem2  24275  polid2i  24558  quad3  27302  4bc2eq6  27390  bpoly3  28200  wallispi2lem1  29864  wallispi2lem2  29865  stirlinglem3  29869  stirlinglem10  29876
  Copyright terms: Public domain W3C validator