Alternate proof of notnotri. The proof via notnotr and [ax-mp] also has three essential steps, but has a total number of steps equal to 8, instead of the present 7, because it has to construct the formula \( \varphi \) twice and the formula \( \neg \neg \varphi \) once, whereas the present proof has to construct the formula \( \varphi \) twice and the formula \( \neg \varphi \) once, and therefore makes only one use of [wn] instead of two. This can be checked by running the Metamath command "MM> SHOW PROOF notnotri / NORMAL". (Contributed by NM, 27-Feb-2008.) (Proof shortened by Wolf Lammen, 15-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.)