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

Theorem 3t3e9 11364
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 11264 . . 3 3 = (2 + 1)
21oveq2i 6816 . 2 (3 · 3) = (3 · (2 + 1))
3 3cn 11279 . . . . 5 3 ∈ ℂ
4 2cn 11275 . . . . 5 2 ∈ ℂ
5 ax-1cn 10178 . . . . 5 1 ∈ ℂ
63, 4, 5adddii 10234 . . . 4 (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7 3t2e6 11363 . . . . 5 (3 · 2) = 6
8 3t1e3 11362 . . . . 5 (3 · 1) = 3
97, 8oveq12i 6817 . . . 4 ((3 · 2) + (3 · 1)) = (6 + 3)
106, 9eqtri 2774 . . 3 (3 · (2 + 1)) = (6 + 3)
11 6p3e9 11354 . . 3 (6 + 3) = 9
1210, 11eqtri 2774 . 2 (3 · (2 + 1)) = 9
132, 12eqtri 2774 1 (3 · 3) = 9
Colors of variables: wff setvar class
Syntax hints:   = wceq 1624  (class class class)co 6805  1c1 10121   + caddc 10123   · cmul 10125  2c2 11254  3c3 11255  6c6 11258  9c9 11261
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rrecex 10192  ax-cnre 10193
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-iota 6004  df-fv 6049  df-ov 6808  df-2 11263  df-3 11264  df-4 11265  df-5 11266  df-6 11267  df-7 11268  df-8 11269  df-9 11270
This theorem is referenced by:  sq3  13147  3dvds  15246  3dvdsOLD  15247  3dvdsdec  15248  3dvdsdecOLD  15249  3dvds2dec  15250  3dvds2decOLD  15251  9nprm  16013  11prm  16016  43prm  16023  83prm  16024  317prm  16027  1259lem2  16033  1259lem4  16035  1259prm  16037  2503lem2  16039  mcubic  24765  log2tlbnd  24863  log2ublem3  24866  log2ub  24867  bposlem9  25208  lgsdir2lem5  25245  ex-lcm  27618  hgt750lem  31030  hgt750lem2  31031  inductionexd  38947  fmtno5lem3  41969  fmtno4prmfac193  41987  fmtno4nprmfac193  41988  127prm  42017
  Copyright terms: Public domain W3C validator