Is this a proof of how law of the excluded middle implies double negation elimination?

676 Views Asked by At

Here is a proof for double negation elimination. I wanna know if it's a proof of how law of excluded middle implies double negation elimination, since there's usage of rule of explosion (ex falso sequitur quodlibet) in this proof and I don't know whether it's an axiom or a derived rule.