Metamath Proof Explorer
Description: Rearrangement of 4 terms in a sum. (Contributed by NM, 9May1999)


Ref 
Expression 

Hypotheses 
add.1 
⊢ 𝐴 ∈ ℂ 


add.2 
⊢ 𝐵 ∈ ℂ 


add.3 
⊢ 𝐶 ∈ ℂ 


add4.4 
⊢ 𝐷 ∈ ℂ 

Assertion 
add4i 
⊢ ( ( 𝐴 + 𝐵 ) + ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 + 𝐶 ) + ( 𝐵 + 𝐷 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

add.1 
⊢ 𝐴 ∈ ℂ 
2 

add.2 
⊢ 𝐵 ∈ ℂ 
3 

add.3 
⊢ 𝐶 ∈ ℂ 
4 

add4.4 
⊢ 𝐷 ∈ ℂ 
5 

add4 
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) + ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 + 𝐶 ) + ( 𝐵 + 𝐷 ) ) ) 
6 
1 2 3 4 5

mp4an 
⊢ ( ( 𝐴 + 𝐵 ) + ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 + 𝐶 ) + ( 𝐵 + 𝐷 ) ) 