Metamath Proof Explorer

Theorem 1m1e0

Description: One minus one equals zero. (Contributed by David A. Wheeler, 7-Jul-2016)

Ref Expression
Assertion 1m1e0 
|- ( 1 - 1 ) = 0

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 1 subidi 
 |-  ( 1 - 1 ) = 0