Metamath Proof Explorer
Description: Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27May2016)


Ref 
Expression 

Hypotheses 
negidd.1 
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) 


pncand.2 
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) 


subaddd.3 
⊢ ( 𝜑 → 𝐶 ∈ ℂ ) 

Assertion 
pnncand 
⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( 𝐵 + 𝐶 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

negidd.1 
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) 
2 

pncand.2 
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) 
3 

subaddd.3 
⊢ ( 𝜑 → 𝐶 ∈ ℂ ) 
4 

pnncan 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( 𝐵 + 𝐶 ) ) 
5 
1 2 3 4

syl3anc 
⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( 𝐵 + 𝐶 ) ) 