Description: 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
ph twice and the formula -. -. ph once, whereas the present
proof has to construct the formula ph twice and the formula
-. ph 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.)