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

Theorem 3t3e9 11793
Description: 3 times 3 equals 9. (Contributed by NM, 11-May-2004.)
Assertion
Ref Expression
3t3e9 (3 · 3) = 9

Proof of Theorem 3t3e9
StepHypRef Expression
1 df-3 11690 . . 3 3 = (2 + 1)
21oveq2i 7156 . 2 (3 · 3) = (3 · (2 + 1))
3 3cn 11707 . . . . 5 3 ∈ ℂ
4 2cn 11701 . . . . 5 2 ∈ ℂ
5 ax-1cn 10584 . . . . 5 1 ∈ ℂ
63, 4, 5adddii 10642 . . . 4 (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7 3t2e6 11792 . . . . 5 (3 · 2) = 6
8 3t1e3 11791 . . . . 5 (3 · 1) = 3
97, 8oveq12i 7157 . . . 4 ((3 · 2) + (3 · 1)) = (6 + 3)
106, 9eqtri 2844 . . 3 (3 · (2 + 1)) = (6 + 3)
11 6p3e9 11786 . . 3 (6 + 3) = 9
1210, 11eqtri 2844 . 2 (3 · (2 + 1)) = 9
132, 12eqtri 2844 1 (3 · 3) = 9
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  (class class class)co 7145  1c1 10527   + caddc 10529   · cmul 10531  2c2 11681  3c3 11682  6c6 11685  9c9 11688
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 2793  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 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7148  df-2 11689  df-3 11690  df-4 11691  df-5 11692  df-6 11693  df-7 11694  df-8 11695  df-9 11696
This theorem is referenced by:  sq3  13551  3dvds  15670  3dvdsdec  15671  3dvds2dec  15672  9nprm  16436  11prm  16438  43prm  16445  83prm  16446  317prm  16449  1259lem2  16455  1259lem4  16457  1259prm  16459  2503lem2  16461  mcubic  25352  log2tlbnd  25451  log2ublem3  25454  log2ub  25455  bposlem9  25796  lgsdir2lem5  25833  ex-lcm  28165  hgt750lem  31822  hgt750lem2  31823  3cubeslem3l  39163  3cubeslem3r  39164  inductionexd  40385  fmtno5lem3  43564  fmtno4prmfac193  43582  fmtno4nprmfac193  43583  127prm  43610  2exp340mod341  43745  9fppr8  43749
  Copyright terms: Public domain W3C validator