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 11890 | . . . . 5 ⊢ 2 = (1 + 1) | |
2 | 1 | oveq2i 7221 | . . . 4 ⊢ (5 + 2) = (5 + (1 + 1)) |
3 | 5cn 11915 | . . . . 5 ⊢ 5 ∈ ℂ | |
4 | ax-1cn 10784 | . . . . 5 ⊢ 1 ∈ ℂ | |
5 | 3, 4, 4 | addassi 10840 | . . . 4 ⊢ ((5 + 1) + 1) = (5 + (1 + 1)) |
6 | 2, 5 | eqtr4i 2768 | . . 3 ⊢ (5 + 2) = ((5 + 1) + 1) |
7 | df-6 11894 | . . . 4 ⊢ 6 = (5 + 1) | |
8 | 7 | oveq1i 7220 | . . 3 ⊢ (6 + 1) = ((5 + 1) + 1) |
9 | 6, 8 | eqtr4i 2768 | . 2 ⊢ (5 + 2) = (6 + 1) |
10 | df-7 11895 | . 2 ⊢ 7 = (6 + 1) | |
11 | 9, 10 | eqtr4i 2768 | 1 ⊢ (5 + 2) = 7 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 (class class class)co 7210 1c1 10727 + caddc 10729 2c2 11882 5c5 11885 6c6 11886 7c7 11887 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 ax-1cn 10784 ax-addcl 10786 ax-addass 10791 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3067 df-v 3407 df-dif 3866 df-un 3868 df-in 3870 df-ss 3880 df-nul 4235 df-if 4437 df-sn 4539 df-pr 4541 df-op 4545 df-uni 4817 df-br 5051 df-iota 6335 df-fv 6385 df-ov 7213 df-2 11890 df-3 11891 df-4 11892 df-5 11893 df-6 11894 df-7 11895 |
This theorem is referenced by: 5p3e8 11984 17prm 16667 prmlem2 16670 37prm 16671 317prm 16676 1259lem1 16681 1259lem2 16682 1259lem4 16684 2503lem2 16688 4001lem1 16691 4001lem4 16694 log2ub 25829 bposlem8 26169 aks4d1p1p4 39810 aks4d1p1p7 39813 ex-decpmul 40025 resqrtvalex 40927 imsqrtvalex 40928 fmtno5lem2 44677 257prm 44684 127prm 44722 |
Copyright terms: Public domain | W3C validator |