| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: One plus one equals two. Using proof-shortening techniques pioneered by Mr. Mel O'Cat, along with the latest supercomputer technology, Prof. Loof Lirpa and colleagues were able to shorten Whitehead and Russell's 360-page proof that 1+1=2 in Principia Mathematica to this remarkable proof only two steps long, thus establishing a new world's record for this famous theorem. (Contributed by Prof. Loof Lirpa, 1-Apr-2008.) |
| Ref | Expression |
|---|---|
| 1p1e2 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-2 6031 |
. 2
| |
| 2 | 1 | eqcomi 1526 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-gen 1004 ax-4 1014 ax-5o 1016 ax-ext 1504 |
| This theorem depends on definitions: df-bi 154 df-an 232 df-cleq 1515 df-2 6031 |