Metamath Proof Explorer

Theorem 7odd

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

Ref Expression
Assertion 7odd 
|- 7 e. Odd

Proof

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