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

Theorem 3t2e6 11391
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 11307 . . 3 3 ∈ ℂ
21times2i 11360 . 2 (3 · 2) = (3 + 3)
3 3p3e6 11373 . 2 (3 + 3) = 6
42, 3eqtri 2782 1 (3 · 2) = 6
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  (class class class)co 6814   + caddc 10151   · cmul 10153  2c2 11282  3c3 11283  6c6 11286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rrecex 10220  ax-cnre 10221
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6817  df-2 11291  df-3 11292  df-4 11293  df-5 11294  df-6 11295
This theorem is referenced by:  3t3e9  11392  8th4div3  11464  halfpm6th  11465  halfthird  11897  fac3  13281  bpoly3  15008  bpoly4  15009  sin01bnd  15134  3lcm2e6woprm  15550  3lcm2e6  15662  prmo3  15967  2exp6  16017  6nprm  16038  7prm  16039  17prm  16046  37prm  16050  83prm  16052  163prm  16054  317prm  16055  631prm  16056  1259lem3  16062  1259lem4  16063  1259lem5  16064  2503lem2  16067  4001lem1  16070  4001lem3  16072  4001prm  16074  sincos6thpi  24487  quart1  24803  log2ublem2  24894  log2ublem3  24895  log2ub  24896  basellem5  25031  basellem8  25034  cht3  25119  ppiublem1  25147  ppiub  25149  bclbnd  25225  bpos1  25228  bposlem8  25236  bposlem9  25237  2lgslem3d  25344  2lgsoddprmlem3d  25358  hgt750lem2  31060  problem4  31890  problem5  31891  pigt3  33733  lhe4.4ex1a  39048  stoweidlem13  40751  257prm  42001  127prm  42043  mod42tp1mod8  42047  6even  42148  2t6m3t4e0  42654  zlmodzxzequa  42813
  Copyright terms: Public domain W3C validator