Metamath Proof Explorer

Theorem nnaword2

Description: Weak ordering property of addition. (Contributed by NM, 9-Nov-2002)

Ref Expression
Assertion nnaword2 
|- ( ( A e. _om /\ B e. _om ) -> A C_ ( B +o A ) )

Proof

Step Hyp Ref Expression
1 nnaword1 
 |-  ( ( A e. _om /\ B e. _om ) -> A C_ ( A +o B ) )
2 nnacom 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A +o B ) = ( B +o A ) )
3 1 2 sseqtrd 
 |-  ( ( A e. _om /\ B e. _om ) -> A C_ ( B +o A ) )