![]() |
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 11416 | . . 3 ⊢ 3 = (2 + 1) | |
2 | 1 | oveq2i 6917 | . 2 ⊢ (3 · 3) = (3 · (2 + 1)) |
3 | 3cn 11433 | . . . . 5 ⊢ 3 ∈ ℂ | |
4 | 2cn 11427 | . . . . 5 ⊢ 2 ∈ ℂ | |
5 | ax-1cn 10311 | . . . . 5 ⊢ 1 ∈ ℂ | |
6 | 3, 4, 5 | adddii 10370 | . . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1)) |
7 | 3t2e6 11525 | . . . . 5 ⊢ (3 · 2) = 6 | |
8 | 3t1e3 11524 | . . . . 5 ⊢ (3 · 1) = 3 | |
9 | 7, 8 | oveq12i 6918 | . . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3) |
10 | 6, 9 | eqtri 2850 | . . 3 ⊢ (3 · (2 + 1)) = (6 + 3) |
11 | 6p3e9 11519 | . . 3 ⊢ (6 + 3) = 9 | |
12 | 10, 11 | eqtri 2850 | . 2 ⊢ (3 · (2 + 1)) = 9 |
13 | 2, 12 | eqtri 2850 | 1 ⊢ (3 · 3) = 9 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1658 (class class class)co 6906 1c1 10254 + caddc 10256 · cmul 10258 2c2 11407 3c3 11408 6c6 11411 9c9 11414 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-resscn 10310 ax-1cn 10311 ax-icn 10312 ax-addcl 10313 ax-mulcl 10315 ax-mulcom 10317 ax-addass 10318 ax-mulass 10319 ax-distr 10320 ax-1rid 10323 ax-cnre 10326 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ral 3123 df-rex 3124 df-rab 3127 df-v 3417 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4660 df-br 4875 df-iota 6087 df-fv 6132 df-ov 6909 df-2 11415 df-3 11416 df-4 11417 df-5 11418 df-6 11419 df-7 11420 df-8 11421 df-9 11422 |
This theorem is referenced by: sq3 13256 3dvds 15430 3dvdsdec 15431 3dvds2dec 15432 9nprm 16186 11prm 16188 43prm 16195 83prm 16196 317prm 16199 1259lem2 16205 1259lem4 16207 1259prm 16209 2503lem2 16211 mcubic 24988 log2tlbnd 25086 log2ublem3 25089 log2ub 25090 bposlem9 25431 lgsdir2lem5 25468 ex-lcm 27874 hgt750lem 31279 hgt750lem2 31280 inductionexd 39294 fmtno5lem3 42298 fmtno4prmfac193 42316 fmtno4nprmfac193 42317 127prm 42346 |
Copyright terms: Public domain | W3C validator |