Metamath Proof Explorer

Theorem 3m1e2

Description: 3 - 1 = 2. (Contributed by FL, 17-Oct-2010) (Revised by NM, 10-Dec-2017) (Proof shortened by AV, 6-Sep-2021)

Ref Expression
Assertion 3m1e2 
|- ( 3 - 1 ) = 2

Proof

Step Hyp Ref Expression
1 2cn 
 |-  2 e. CC
2 ax-1cn 
 |-  1 e. CC
3 df-3 
 |-  3 = ( 2 + 1 )
4 1 2 3 mvrraddi 
 |-  ( 3 - 1 ) = 2