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

Theorem 3t3e9 11165
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 11065 . . 3 3 = (2 + 1)
21oveq2i 6646 . 2 (3 · 3) = (3 · (2 + 1))
3 3cn 11080 . . . . 5 3 ∈ ℂ
4 2cn 11076 . . . . 5 2 ∈ ℂ
5 ax-1cn 9979 . . . . 5 1 ∈ ℂ
63, 4, 5adddii 10035 . . . 4 (3 · (2 + 1)) = ((3 · 2) + (3 · 1))
7 3t2e6 11164 . . . . 5 (3 · 2) = 6
8 3t1e3 11163 . . . . 5 (3 · 1) = 3
97, 8oveq12i 6647 . . . 4 ((3 · 2) + (3 · 1)) = (6 + 3)
106, 9eqtri 2642 . . 3 (3 · (2 + 1)) = (6 + 3)
11 6p3e9 11155 . . 3 (6 + 3) = 9
1210, 11eqtri 2642 . 2 (3 · (2 + 1)) = 9
132, 12eqtri 2642 1 (3 · 3) = 9
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  (class class class)co 6635  1c1 9922   + caddc 9924   · cmul 9926  2c2 11055  3c3 11056  6c6 11059  9c9 11062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rrecex 9993  ax-cnre 9994
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-iota 5839  df-fv 5884  df-ov 6638  df-2 11064  df-3 11065  df-4 11066  df-5 11067  df-6 11068  df-7 11069  df-8 11070  df-9 11071
This theorem is referenced by:  sq3  12944  3dvds  15033  3dvdsOLD  15034  3dvdsdec  15035  3dvdsdecOLD  15036  3dvds2dec  15037  3dvds2decOLD  15038  9nprm  15800  11prm  15803  43prm  15810  83prm  15811  317prm  15814  1259lem2  15820  1259lem4  15822  1259prm  15824  2503lem2  15826  mcubic  24555  log2tlbnd  24653  log2ublem3  24656  log2ub  24657  bposlem9  24998  lgsdir2lem5  25035  ex-lcm  27285  hgt750lem  30703  hgt750lem2  30704  inductionexd  38273  fmtno5lem3  41232  fmtno4prmfac193  41250  fmtno4nprmfac193  41251  127prm  41280
  Copyright terms: Public domain W3C validator