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 11702 | . . 3 ⊢ 3 = (2 + 1) | |
2 | 1 | oveq2i 7167 | . 2 ⊢ (3 · 3) = (3 · (2 + 1)) |
3 | 3cn 11719 | . . . . 5 ⊢ 3 ∈ ℂ | |
4 | 2cn 11713 | . . . . 5 ⊢ 2 ∈ ℂ | |
5 | ax-1cn 10595 | . . . . 5 ⊢ 1 ∈ ℂ | |
6 | 3, 4, 5 | adddii 10653 | . . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1)) |
7 | 3t2e6 11804 | . . . . 5 ⊢ (3 · 2) = 6 | |
8 | 3t1e3 11803 | . . . . 5 ⊢ (3 · 1) = 3 | |
9 | 7, 8 | oveq12i 7168 | . . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3) |
10 | 6, 9 | eqtri 2844 | . . 3 ⊢ (3 · (2 + 1)) = (6 + 3) |
11 | 6p3e9 11798 | . . 3 ⊢ (6 + 3) = 9 | |
12 | 10, 11 | eqtri 2844 | . 2 ⊢ (3 · (2 + 1)) = 9 |
13 | 2, 12 | eqtri 2844 | 1 ⊢ (3 · 3) = 9 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 (class class class)co 7156 1c1 10538 + caddc 10540 · cmul 10542 2c2 11693 3c3 11694 6c6 11697 9c9 11700 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-mulcl 10599 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-1rid 10607 ax-cnre 10610 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-iota 6314 df-fv 6363 df-ov 7159 df-2 11701 df-3 11702 df-4 11703 df-5 11704 df-6 11705 df-7 11706 df-8 11707 df-9 11708 |
This theorem is referenced by: sq3 13562 3dvds 15680 3dvdsdec 15681 3dvds2dec 15682 9nprm 16446 11prm 16448 43prm 16455 83prm 16456 317prm 16459 1259lem2 16465 1259lem4 16467 1259prm 16469 2503lem2 16471 mcubic 25425 log2tlbnd 25523 log2ublem3 25526 log2ub 25527 bposlem9 25868 lgsdir2lem5 25905 ex-lcm 28237 hgt750lem 31922 hgt750lem2 31923 3cubeslem3l 39303 3cubeslem3r 39304 inductionexd 40525 fmtno5lem3 43737 fmtno4prmfac193 43755 fmtno4nprmfac193 43756 127prm 43783 2exp340mod341 43918 9fppr8 43922 |
Copyright terms: Public domain | W3C validator |