MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3t2e6 Unicode version

Theorem 3t2e6 10060
Description: 3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.)
Assertion
Ref Expression
3t2e6  |-  ( 3  x.  2 )  =  6

Proof of Theorem 3t2e6
StepHypRef Expression
1 3cn 10004 . . 3  |-  3  e.  CC
21times2i 10034 . 2  |-  ( 3  x.  2 )  =  ( 3  +  3 )
3 3p3e6 10044 . 2  |-  ( 3  +  3 )  =  6
42, 3eqtri 2407 1  |-  ( 3  x.  2 )  =  6
Colors of variables: wff set class
Syntax hints:    = wceq 1649  (class class class)co 6020    + caddc 8926    x. cmul 8928   2c2 9981   3c3 9982   6c6 9985
This theorem is referenced by:  3t3e9  10061  8th4div3  10123  halfpm6th  10124  fac3  11500  sin01bnd  12713  6nprm  13359  7prm  13360  17prm  13366  37prm  13370  83prm  13372  163prm  13374  317prm  13375  631prm  13376  1259lem3  13379  1259lem4  13380  1259lem5  13381  2503lem2  13384  4001lem1  13387  4001lem3  13389  4001prm  13391  sincos6thpi  20290  quart1  20563  log2ublem2  20654  log2ublem3  20655  log2ub  20656  basellem5  20734  basellem8  20737  cht3  20823  ppiublem1  20853  ppiub  20855  bclbnd  20931  bpos1  20934  bposlem8  20942  bposlem9  20943  halfthird  24984  bpoly3  25818  bpoly4  25819  lhe4.4ex1a  27215  stoweidlem13  27430
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-resscn 8980  ax-1cn 8981  ax-icn 8982  ax-addcl 8983  ax-addrcl 8984  ax-mulcl 8985  ax-mulrcl 8986  ax-mulcom 8987  ax-addass 8988  ax-mulass 8989  ax-distr 8990  ax-i2m1 8991  ax-1ne0 8992  ax-1rid 8993  ax-rrecex 8995  ax-cnre 8996
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-iota 5358  df-fv 5402  df-ov 6023  df-2 9990  df-3 9991  df-4 9992  df-5 9993  df-6 9994
  Copyright terms: Public domain W3C validator