Description: If two formulas are equivalent for all x , then nonfreeness of x
in one of them is equivalent to nonfreeness in the other. Compare
nfbiit . From this and bj-nnfim and bj-nnfnt , one can prove
analogous nonfreeness conservation results for other propositional
operators. The antecedent is in the "strong necessity" modality of modal
logic (see also bj-nnftht ) in order not to require sp (modal T).
(Contributed by BJ, 27-Aug-2023)