Metamath Proof Explorer

Theorem pncan3

Description: Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005) (Proof shortened by Steven Nguyen, 8-Jan-2023)

Ref Expression
Assertion pncan3 
|- ( ( A e. CC /\ B e. CC ) -> ( A + ( B - A ) ) = B )

Proof

Step Hyp Ref Expression
1 subcl 
 |-  ( ( B e. CC /\ A e. CC ) -> ( B - A ) e. CC )
2 eqid 
 |-  ( B - A ) = ( B - A )
3 subadd 
 |-  ( ( B e. CC /\ A e. CC /\ ( B - A ) e. CC ) -> ( ( B - A ) = ( B - A ) <-> ( A + ( B - A ) ) = B ) )
4 2 3 mpbii 
 |-  ( ( B e. CC /\ A e. CC /\ ( B - A ) e. CC ) -> ( A + ( B - A ) ) = B )
5 1 4 mpd3an3 
 |-  ( ( B e. CC /\ A e. CC ) -> ( A + ( B - A ) ) = B )
6 5 ancoms 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + ( B - A ) ) = B )