Could anyone please explain what an excluded middle from the following derivation is?
I should add that the law of excluded middle is just a name for formulas of the form . It does not automatically mean that it has to be used as an axiom. In fact, in natural deduction it is usually derivable using the inference rule of double-negation elimination. Pure natural deduction does not have axioms.