Description: Alternate proof of notnotri 133. The proof via notnotr 132 and ax-mp 5
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
𝜑 twice and the formula ¬ ¬ 𝜑 once, whereas the present
proof has to construct the formula 𝜑 twice and the formula
¬ 𝜑 once, and therefore makes only one
use of wn 3 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.) |