Description: New nonfreeness implies old nonfreeness on implicational calculus (the
proof indicates it uses ax-3 because of set.mm's definition of the
biconditional, but the proof actually holds in minimal implicational
calculus). (Contributed by BJ, 28-Jul-2023) The proof should not rely
on df-nf except via df-nf directly.
(Proof modification is discouraged.)