Metamath Proof Explorer


Theorem 7odd

Description: 7 is an odd number. (Contributed by AV, 20-Jul-2020)

Ref Expression
Assertion 7odd 7 Odd

Proof

Step Hyp Ref Expression
1 df-7 7 = 6 + 1
2 6even 6 Even
3 evenp1odd 6 Even 6 + 1 Odd
4 2 3 ax-mp 6 + 1 Odd
5 1 4 eqeltri 7 Odd