Metamath Proof Explorer


Theorem 3odd

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

Ref Expression
Assertion 3odd
|- 3 e. Odd

Proof

Step Hyp Ref Expression
1 2evenALTV
 |-  2 e. Even
2 df-3
 |-  3 = ( 2 + 1 )
3 evenp1odd
 |-  ( 2 e. Even -> ( 2 + 1 ) e. Odd )
4 2 3 eqeltrid
 |-  ( 2 e. Even -> 3 e. Odd )
5 1 4 ax-mp
 |-  3 e. Odd