![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3p2e5 | Structured version Visualization version Unicode version |
Description: 3 + 2 = 5. (Contributed by NM, 11-May-2004.) |
Ref | Expression |
---|---|
3p2e5 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2 10675 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | oveq2i 6306 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 3cn 10691 |
. . . . 5
![]() ![]() ![]() ![]() | |
4 | ax-1cn 9602 |
. . . . 5
![]() ![]() ![]() ![]() | |
5 | 3, 4, 4 | addassi 9656 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 2, 5 | eqtr4i 2478 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | df-4 10677 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 7 | oveq1i 6305 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 6, 8 | eqtr4i 2478 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | df-5 10678 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 9, 10 | eqtr4i 2478 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-resscn 9601 ax-1cn 9602 ax-icn 9603 ax-addcl 9604 ax-addrcl 9605 ax-mulcl 9606 ax-mulrcl 9607 ax-addass 9609 ax-i2m1 9612 ax-1ne0 9613 ax-rrecex 9616 ax-cnre 9617 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-ral 2744 df-rex 2745 df-rab 2748 df-v 3049 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3734 df-if 3884 df-sn 3971 df-pr 3973 df-op 3977 df-uni 4202 df-br 4406 df-iota 5549 df-fv 5593 df-ov 6298 df-2 10675 df-3 10676 df-4 10677 df-5 10678 |
This theorem is referenced by: 3p3e6 10750 2exp16 15073 prmlem1a 15090 5prm 15092 prmlem2 15103 1259lem1 15114 1259lem4 15117 1259prm 15119 4001lem1 15124 4001lem4 15127 birthday 23892 ppiub 24144 bposlem6 24229 bposlem9 24232 fib5 29250 kur14lem8 29948 problem1 30309 41prothprmlem2 38928 linevalexample 40292 |
Copyright terms: Public domain | W3C validator |