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 2841 1 (3 · 2) = 6
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  (class class class)co 7145   + caddc 10528   · cmul 10530  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 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-mulcl 10587  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-1rid 10595  ax-cnre 10598
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148  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  13628  bpoly3  15400  bpoly4  15401  sin01bnd  15526  3lcm2e6woprm  15947  3lcm2e6  16060  prmo3  16365  2exp6  16410  6nprm  16431  7prm  16432  17prm  16438  37prm  16442  83prm  16444  163prm  16446  317prm  16447  631prm  16448  1259lem3  16454  1259lem4  16455  1259lem5  16456  2503lem2  16459  4001lem1  16462  4001lem3  16464  4001prm  16466  sincos6thpi  25028  pigt3  25030  quart1  25361  log2ublem2  25452  log2ublem3  25453  log2ub  25454  basellem5  25589  basellem8  25592  cht3  25677  ppiublem1  25705  ppiub  25707  bclbnd  25783  bpos1  25786  bposlem8  25794  bposlem9  25795  2lgslem3d  25902  2lgsoddprmlem3d  25916  hgt750lem2  31822  problem4  32808  problem5  32809  3cubeslem3l  39161  3cubeslem3r  39162  lhe4.4ex1a  40538  stoweidlem13  42175  257prm  43600  127prm  43640  mod42tp1mod8  43644  6even  43753  2exp340mod341  43775  2t6m3t4e0  44324  zlmodzxzequa  44479
  Copyright terms: Public domain W3C validator