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

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

Proof of Theorem 3t2e6
StepHypRef Expression
1 3cn 11706 . . 3 3 ∈ ℂ
21times2i 11764 . 2 (3 · 2) = (3 + 3)
3 3p3e6 11777 . 2 (3 + 3) = 6
42, 3eqtri 2845 1 (3 · 2) = 6
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  (class class class)co 7140   + caddc 10529   · cmul 10531  2c2 11680  3c3 11681  6c6 11684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-ral 3135  df-rex 3136  df-v 3471  df-un 3913  df-in 3915  df-ss 3925  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-iota 6293  df-fv 6342  df-ov 7143  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692
This theorem is referenced by:  3t3e9  11792  8th4div3  11845  halfpm6th  11846  halfthird  12229  fac3  13636  bpoly3  15403  bpoly4  15404  sin01bnd  15529  3lcm2e6woprm  15948  3lcm2e6  16061  prmo3  16366  2exp6  16412  6nprm  16434  7prm  16435  17prm  16441  37prm  16445  83prm  16447  163prm  16449  317prm  16450  631prm  16451  1259lem3  16457  1259lem4  16458  1259lem5  16459  2503lem2  16462  4001lem1  16465  4001lem3  16467  4001prm  16469  sincos6thpi  25106  pigt3  25108  quart1  25440  log2ublem2  25531  log2ublem3  25532  log2ub  25533  basellem5  25668  basellem8  25671  cht3  25756  ppiublem1  25784  ppiub  25786  bclbnd  25862  bpos1  25865  bposlem8  25873  bposlem9  25874  2lgslem3d  25981  2lgsoddprmlem3d  25995  hgt750lem2  31997  problem4  32985  problem5  32986  3cubeslem3l  39557  3cubeslem3r  39558  lhe4.4ex1a  40967  stoweidlem13  42594  257prm  44017  127prm  44055  mod42tp1mod8  44059  6even  44168  2exp340mod341  44190  2t6m3t4e0  44689  zlmodzxzequa  44844
  Copyright terms: Public domain W3C validator