![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > 2p2e4 | Structured version Unicode version |
Description: Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: http://us.metamath.org/mpeuni/mmset.html#trivia. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
2p2e4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2 10492 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | oveq2i 6212 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-4 10494 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-3 10493 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | oveq1i 6211 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 2cn 10504 |
. . . 4
![]() ![]() ![]() ![]() | |
7 | ax-1cn 9452 |
. . . 4
![]() ![]() ![]() ![]() | |
8 | 6, 7, 7 | addassi 9506 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 3, 5, 8 | 3eqtri 2487 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 2, 9 | eqtr4i 2486 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-resscn 9451 ax-1cn 9452 ax-icn 9453 ax-addcl 9454 ax-addrcl 9455 ax-mulcl 9456 ax-mulrcl 9457 ax-addass 9459 ax-i2m1 9462 ax-1ne0 9463 ax-rrecex 9466 ax-cnre 9467 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-ral 2804 df-rex 2805 df-rab 2808 df-v 3080 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-nul 3747 df-if 3901 df-sn 3987 df-pr 3989 df-op 3993 df-uni 4201 df-br 4402 df-iota 5490 df-fv 5535 df-ov 6204 df-2 10492 df-3 10493 df-4 10494 |
This theorem is referenced by: 2t2e4 10583 i4 12086 ef01bndlem 13587 pythagtriplem1 14002 prmlem2 14266 43prm 14268 1259lem4 14277 2503lem1 14280 2503lem2 14281 2503lem3 14282 4001lem1 14284 4001lem4 14287 quart1lem 22384 log2ub 22478 4bc2eq6 27536 bpoly4 28347 fsumcube 28348 wallispi2lem1 30015 stirlinglem8 30025 2t6m3t4e0 30889 2p2ne5 31483 |
Copyright terms: Public domain | W3C validator |