Metamath Proof Explorer


Theorem 1p1e2apr1

Description: One plus one equals two. Using proof-shortening techniques pioneered by Mr. Mel L. 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 inPrincipia 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) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 1p1e2apr1
|- ( 1 + 1 ) = 2

Proof

Step Hyp Ref Expression
1 df-2
 |-  2 = ( 1 + 1 )
2 1 eqcomi
 |-  ( 1 + 1 ) = 2