Description: 2  1 = 1. The result is on the righthandside to be consistent with similar proofs like 4p4e8 . (Contributed by David A. Wheeler, 4Jan2017)
Ref  Expression  

Assertion  2m1e1   ( 2  1 ) = 1 
Step  Hyp  Ref  Expression 

1  2cn   2 e. CC 

2  ax1cn   1 e. CC 

3  1p1e2   ( 1 + 1 ) = 2 

4  1 2 2 3  subaddrii   ( 2  1 ) = 1 