Metamath Proof Explorer

Theorem repnpcan

Description: Cancellation law for addition and real subtraction. Compare pnpcan . (Contributed by Steven Nguyen, 19-May-2023)

Ref Expression
Assertion repnpcan 
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) -R ( A + C ) ) = ( B -R C ) )

Proof

Step Hyp Ref Expression
1 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
2 resubsub4 
 |-  ( ( ( A + B ) e. RR /\ A e. RR /\ C e. RR ) -> ( ( ( A + B ) -R A ) -R C ) = ( ( A + B ) -R ( A + C ) ) )
3 1 2 stoic4a 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( ( A + B ) -R A ) -R C ) = ( ( A + B ) -R ( A + C ) ) )
4 repncan2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) -R A ) = B )
5 4 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) -R A ) = B )
6 5 oveq1d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( ( A + B ) -R A ) -R C ) = ( B -R C ) )
7 3 6 eqtr3d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) -R ( A + C ) ) = ( B -R C ) )