Metamath Proof Explorer

Theorem nnacan

Description: Cancellation law for addition of natural numbers. (Contributed by NM, 27-Oct-1995) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnacan 
|- ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( A +o B ) = ( A +o C ) <-> B = C ) )

Proof

Step Hyp Ref Expression
1 nnaword 
 |-  ( ( B e. _om /\ C e. _om /\ A e. _om ) -> ( B C_ C <-> ( A +o B ) C_ ( A +o C ) ) )
2 1 3comr 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( B C_ C <-> ( A +o B ) C_ ( A +o C ) ) )
3 nnaword 
 |-  ( ( C e. _om /\ B e. _om /\ A e. _om ) -> ( C C_ B <-> ( A +o C ) C_ ( A +o B ) ) )
4 3 3com13 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( C C_ B <-> ( A +o C ) C_ ( A +o B ) ) )
5 2 4 anbi12d 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( B C_ C /\ C C_ B ) <-> ( ( A +o B ) C_ ( A +o C ) /\ ( A +o C ) C_ ( A +o B ) ) ) )
6 5 bicomd 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( ( A +o B ) C_ ( A +o C ) /\ ( A +o C ) C_ ( A +o B ) ) <-> ( B C_ C /\ C C_ B ) ) )
7 eqss 
 |-  ( ( A +o B ) = ( A +o C ) <-> ( ( A +o B ) C_ ( A +o C ) /\ ( A +o C ) C_ ( A +o B ) ) )
8 eqss 
 |-  ( B = C <-> ( B C_ C /\ C C_ B ) )
9 6 7 8 3bitr4g 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( A +o B ) = ( A +o C ) <-> B = C ) )