Metamath Proof Explorer


Theorem 4p1e5

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

Ref Expression
Assertion 4p1e5
|- ( 4 + 1 ) = 5

Proof

Step Hyp Ref Expression
1 df-5
 |-  5 = ( 4 + 1 )
2 1 eqcomi
 |-  ( 4 + 1 ) = 5