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

Theorem 3t2e6 10727
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 10650 . . 3  |-  3  e.  CC
21times2i 10697 . 2  |-  ( 3  x.  2 )  =  ( 3  +  3 )
3 3p3e6 10709 . 2  |-  ( 3  +  3 )  =  6
42, 3eqtri 2431 1  |-  ( 3  x.  2 )  =  6
Colors of variables: wff setvar class
Syntax hints:    = wceq 1405  (class class class)co 6277    + caddc 9524    x. cmul 9526   2c2 10625   3c3 10626   6c6 10629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-resscn 9578  ax-1cn 9579  ax-icn 9580  ax-addcl 9581  ax-addrcl 9582  ax-mulcl 9583  ax-mulrcl 9584  ax-mulcom 9585  ax-addass 9586  ax-mulass 9587  ax-distr 9588  ax-i2m1 9589  ax-1ne0 9590  ax-1rid 9591  ax-rrecex 9593  ax-cnre 9594
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-iota 5532  df-fv 5576  df-ov 6280  df-2 10634  df-3 10635  df-4 10636  df-5 10637  df-6 10638
This theorem is referenced by:  3t3e9  10728  8th4div3  10799  halfpm6th  10800  halfthird  11124  fac3  12402  bpoly3  14001  bpoly4  14002  sin01bnd  14127  2exp6  14779  6nprm  14802  7prm  14803  17prm  14809  37prm  14813  83prm  14815  163prm  14817  317prm  14818  631prm  14819  1259lem3  14822  1259lem4  14823  1259lem5  14824  2503lem2  14827  4001lem1  14830  4001lem3  14832  4001prm  14834  sincos6thpi  23198  quart1  23510  log2ublem2  23601  log2ublem3  23602  log2ub  23603  basellem5  23737  basellem8  23740  cht3  23826  ppiublem1  23856  ppiub  23858  bclbnd  23934  bpos1  23937  bposlem8  23945  bposlem9  23946  problem4  29861  problem5  29862  3lcm2e6  36047  lhe4.4ex1a  36062  stoweidlem13  37144  6even  37772  2t6m3t4e0  38429  zlmodzxzequa  38589
  Copyright terms: Public domain W3C validator