Metamath Proof Explorer


Theorem 6m1e5

Description: 6 - 1 = 5. (Contributed by AV, 6-Sep-2021)

Ref Expression
Assertion 6m1e5
|- ( 6 - 1 ) = 5

Proof

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