![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 7p2e9 | Structured version Visualization version GIF version |
Description: 7 + 2 = 9. (Contributed by NM, 11-May-2004.) |
Ref | Expression |
---|---|
7p2e9 | ⊢ (7 + 2) = 9 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2 12306 | . . . . 5 ⊢ 2 = (1 + 1) | |
2 | 1 | oveq2i 7431 | . . . 4 ⊢ (7 + 2) = (7 + (1 + 1)) |
3 | 7cn 12337 | . . . . 5 ⊢ 7 ∈ ℂ | |
4 | ax-1cn 11197 | . . . . 5 ⊢ 1 ∈ ℂ | |
5 | 3, 4, 4 | addassi 11255 | . . . 4 ⊢ ((7 + 1) + 1) = (7 + (1 + 1)) |
6 | 2, 5 | eqtr4i 2759 | . . 3 ⊢ (7 + 2) = ((7 + 1) + 1) |
7 | df-8 12312 | . . . 4 ⊢ 8 = (7 + 1) | |
8 | 7 | oveq1i 7430 | . . 3 ⊢ (8 + 1) = ((7 + 1) + 1) |
9 | 6, 8 | eqtr4i 2759 | . 2 ⊢ (7 + 2) = (8 + 1) |
10 | df-9 12313 | . 2 ⊢ 9 = (8 + 1) | |
11 | 9, 10 | eqtr4i 2759 | 1 ⊢ (7 + 2) = 9 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 (class class class)co 7420 1c1 11140 + caddc 11142 2c2 12298 7c7 12303 8c8 12304 9c9 12305 |
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 2699 ax-1cn 11197 ax-addcl 11199 ax-addass 11204 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-rab 3430 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-br 5149 df-iota 6500 df-fv 6556 df-ov 7423 df-2 12306 df-3 12307 df-4 12308 df-5 12309 df-6 12310 df-7 12311 df-8 12312 df-9 12313 |
This theorem is referenced by: 7p3e10 12783 7t7e49 12822 cos2bnd 16165 prmlem2 17089 139prm 17093 1259lem2 17101 1259lem3 17102 1259lem4 17103 1259lem5 17104 2503lem2 17107 4001lem4 17113 hgt750lem2 34284 aks4d1p1p7 41545 fmtno5lem4 46896 fmtno5fac 46922 139prmALT 46936 |
Copyright terms: Public domain | W3C validator |