If you use ¬¬ϕ = ϕ in your proof, you loose constructivity. Why would you care about this? Simplifying a bit, in a constructive proof, every existential state

If you use ¬¬ϕ = ϕ in your proof, you loose constructivity. Why would you care about this? Simplifying a bit, in a constructive proof, every existential statement ∃x.ϕ comes with a witness c such that ϕ is true when x is replaced by c. Likewise, in a logical disjunction ϕ \/ Ψ comes with information whether ϕ is true or Ψ. If your proof is not constructive, you may not be able to get this information from the proof. In other words, a constructive proof is nicer than a non-constructive proof. OTOH, non-constructive proofs tend to be easier to find, indeed some theorems have only non-constructive proofs. Moreover, non-constructive can sometimes be shorter than constructive proofs of the same statement.