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