![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3t3e9 | Structured version Visualization version GIF version |
Description: 3 times 3 equals 9. (Contributed by NM, 11-May-2004.) |
Ref | Expression |
---|---|
3t3e9 | ⊢ (3 · 3) = 9 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3 12328 | . . 3 ⊢ 3 = (2 + 1) | |
2 | 1 | oveq2i 7435 | . 2 ⊢ (3 · 3) = (3 · (2 + 1)) |
3 | 3cn 12345 | . . . . 5 ⊢ 3 ∈ ℂ | |
4 | 2cn 12339 | . . . . 5 ⊢ 2 ∈ ℂ | |
5 | ax-1cn 11216 | . . . . 5 ⊢ 1 ∈ ℂ | |
6 | 3, 4, 5 | adddii 11276 | . . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1)) |
7 | 3t2e6 12430 | . . . . 5 ⊢ (3 · 2) = 6 | |
8 | 3t1e3 12429 | . . . . 5 ⊢ (3 · 1) = 3 | |
9 | 7, 8 | oveq12i 7436 | . . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3) |
10 | 6, 9 | eqtri 2754 | . . 3 ⊢ (3 · (2 + 1)) = (6 + 3) |
11 | 6p3e9 12424 | . . 3 ⊢ (6 + 3) = 9 | |
12 | 10, 11 | eqtri 2754 | . 2 ⊢ (3 · (2 + 1)) = 9 |
13 | 2, 12 | eqtri 2754 | 1 ⊢ (3 · 3) = 9 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 (class class class)co 7424 1c1 11159 + caddc 11161 · cmul 11163 2c2 12319 3c3 12320 6c6 12323 9c9 12326 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-resscn 11215 ax-1cn 11216 ax-icn 11217 ax-addcl 11218 ax-mulcl 11220 ax-mulcom 11222 ax-addass 11223 ax-mulass 11224 ax-distr 11225 ax-1rid 11228 ax-cnre 11231 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rex 3061 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-br 5154 df-iota 6506 df-fv 6562 df-ov 7427 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 |
This theorem is referenced by: sq3 14216 3dvds 16333 3dvdsdec 16334 3dvds2dec 16335 9nprm 17115 11prm 17117 43prm 17124 83prm 17125 317prm 17128 1259lem2 17134 1259lem4 17136 1259prm 17138 2503lem2 17140 mcubic 26875 log2tlbnd 26973 log2ublem3 26976 log2ub 26977 bposlem9 27321 lgsdir2lem5 27358 ex-lcm 30391 hgt750lem 34497 hgt750lem2 34498 3lexlogpow2ineq2 41758 3lexlogpow5ineq5 41759 3cubeslem3l 42343 3cubeslem3r 42344 inductionexd 43822 fmtno5lem3 47127 fmtno4prmfac193 47145 fmtno4nprmfac193 47146 127prm 47171 2exp340mod341 47305 9fppr8 47309 |
Copyright terms: Public domain | W3C validator |