Metamath Proof Explorer


Theorem 8p1e9

Description: 8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015)

Ref Expression
Assertion 8p1e9
|- ( 8 + 1 ) = 9

Proof

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