![]() |
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 12272 | . . 3 ⊢ 3 = (2 + 1) | |
2 | 1 | oveq2i 7416 | . 2 ⊢ (3 · 3) = (3 · (2 + 1)) |
3 | 3cn 12289 | . . . . 5 ⊢ 3 ∈ ℂ | |
4 | 2cn 12283 | . . . . 5 ⊢ 2 ∈ ℂ | |
5 | ax-1cn 11164 | . . . . 5 ⊢ 1 ∈ ℂ | |
6 | 3, 4, 5 | adddii 11222 | . . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1)) |
7 | 3t2e6 12374 | . . . . 5 ⊢ (3 · 2) = 6 | |
8 | 3t1e3 12373 | . . . . 5 ⊢ (3 · 1) = 3 | |
9 | 7, 8 | oveq12i 7417 | . . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3) |
10 | 6, 9 | eqtri 2760 | . . 3 ⊢ (3 · (2 + 1)) = (6 + 3) |
11 | 6p3e9 12368 | . . 3 ⊢ (6 + 3) = 9 | |
12 | 10, 11 | eqtri 2760 | . 2 ⊢ (3 · (2 + 1)) = 9 |
13 | 2, 12 | eqtri 2760 | 1 ⊢ (3 · 3) = 9 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 (class class class)co 7405 1c1 11107 + caddc 11109 · cmul 11111 2c2 12263 3c3 12264 6c6 12267 9c9 12270 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-mulcl 11168 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-1rid 11176 ax-cnre 11179 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rex 3071 df-rab 3433 df-v 3476 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-iota 6492 df-fv 6548 df-ov 7408 df-2 12271 df-3 12272 df-4 12273 df-5 12274 df-6 12275 df-7 12276 df-8 12277 df-9 12278 |
This theorem is referenced by: sq3 14158 3dvds 16270 3dvdsdec 16271 3dvds2dec 16272 9nprm 17042 11prm 17044 43prm 17051 83prm 17052 317prm 17055 1259lem2 17061 1259lem4 17063 1259prm 17065 2503lem2 17067 mcubic 26341 log2tlbnd 26439 log2ublem3 26442 log2ub 26443 bposlem9 26784 lgsdir2lem5 26821 ex-lcm 29700 hgt750lem 33651 hgt750lem2 33652 3lexlogpow2ineq2 40912 3lexlogpow5ineq5 40913 3cubeslem3l 41409 3cubeslem3r 41410 inductionexd 42891 fmtno5lem3 46209 fmtno4prmfac193 46227 fmtno4nprmfac193 46228 127prm 46253 2exp340mod341 46387 9fppr8 46391 |
Copyright terms: Public domain | W3C validator |