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

Theorem 4t2e8 10710
Description: 4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.)
Assertion
Ref Expression
4t2e8  |-  ( 4  x.  2 )  =  8

Proof of Theorem 4t2e8
StepHypRef Expression
1 4cn 10634 . . 3  |-  4  e.  CC
21times2i 10678 . 2  |-  ( 4  x.  2 )  =  ( 4  +  4 )
3 4p4e8 10693 . 2  |-  ( 4  +  4 )  =  8
42, 3eqtri 2486 1  |-  ( 4  x.  2 )  =  8
Colors of variables: wff setvar class
Syntax hints:    = wceq 1395  (class class class)co 6296    + caddc 9512    x. cmul 9514   2c2 10606   4c4 10608   8c8 10612
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rrecex 9581  ax-cnre 9582
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-iota 5557  df-fv 5602  df-ov 6299  df-2 10615  df-3 10616  df-4 10617  df-5 10618  df-6 10619  df-7 10620  df-8 10621
This theorem is referenced by:  8th4div3  10780  4t3e12  11072  cu2  12269  cos2bnd  13935  2exp8  14586  8nprm  14609  19prm  14615  139prm  14621  1259lem2  14626  1259lem3  14627  1259lem4  14628  1259lem5  14629  2503lem1  14631  2503lem2  14632  4001lem1  14635  4001lem2  14636  4001lem3  14637  4001lem4  14638  quart1lem  23312  quart1  23313  quartlem1  23314  log2tlbnd  23402  log2ub  23406  bpos1  23684  bposlem8  23692  lgsdir2lem2  23725  chebbnd1lem2  23781  chebbnd1lem3  23782  pntlemr  23913
  Copyright terms: Public domain W3C validator