Metamath Proof Explorer


Theorem 3odd

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

Ref Expression
Assertion 3odd 3 ∈ Odd

Proof

Step Hyp Ref Expression
1 2evenALTV 2 ∈ Even
2 df-3 3 = ( 2 + 1 )
3 evenp1odd ( 2 ∈ Even → ( 2 + 1 ) ∈ Odd )
4 2 3 eqeltrid ( 2 ∈ Even → 3 ∈ Odd )
5 1 4 ax-mp 3 ∈ Odd