![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 5p2e7 | Structured version Visualization version GIF version |
Description: 5 + 2 = 7. (Contributed by NM, 11-May-2004.) |
Ref | Expression |
---|---|
5p2e7 | ⊢ (5 + 2) = 7 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2 12282 | . . . . 5 ⊢ 2 = (1 + 1) | |
2 | 1 | oveq2i 7423 | . . . 4 ⊢ (5 + 2) = (5 + (1 + 1)) |
3 | 5cn 12307 | . . . . 5 ⊢ 5 ∈ ℂ | |
4 | ax-1cn 11174 | . . . . 5 ⊢ 1 ∈ ℂ | |
5 | 3, 4, 4 | addassi 11231 | . . . 4 ⊢ ((5 + 1) + 1) = (5 + (1 + 1)) |
6 | 2, 5 | eqtr4i 2762 | . . 3 ⊢ (5 + 2) = ((5 + 1) + 1) |
7 | df-6 12286 | . . . 4 ⊢ 6 = (5 + 1) | |
8 | 7 | oveq1i 7422 | . . 3 ⊢ (6 + 1) = ((5 + 1) + 1) |
9 | 6, 8 | eqtr4i 2762 | . 2 ⊢ (5 + 2) = (6 + 1) |
10 | df-7 12287 | . 2 ⊢ 7 = (6 + 1) | |
11 | 9, 10 | eqtr4i 2762 | 1 ⊢ (5 + 2) = 7 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1540 (class class class)co 7412 1c1 11117 + caddc 11119 2c2 12274 5c5 12277 6c6 12278 7c7 12279 |
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 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 ax-1cn 11174 ax-addcl 11176 ax-addass 11181 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-iota 6495 df-fv 6551 df-ov 7415 df-2 12282 df-3 12283 df-4 12284 df-5 12285 df-6 12286 df-7 12287 |
This theorem is referenced by: 5p3e8 12376 17prm 17057 prmlem2 17060 37prm 17061 317prm 17066 1259lem1 17071 1259lem2 17072 1259lem4 17074 2503lem2 17078 4001lem1 17081 4001lem4 17084 log2ub 26795 bposlem8 27137 aks4d1p1p4 41403 aks4d1p1p7 41406 ex-decpmul 41669 resqrtvalex 42859 imsqrtvalex 42860 fmtno5lem2 46681 257prm 46688 127prm 46726 |
Copyright terms: Public domain | W3C validator |