Metamath Proof Explorer


Theorem 3odd

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

Ref Expression
Assertion 3odd 3Odd

Proof

Step Hyp Ref Expression
1 2evenALTV 2Even
2 df-3 3=2+1
3 evenp1odd 2Even2+1Odd
4 2 3 eqeltrid 2Even3Odd
5 1 4 ax-mp 3Odd