Theorem bj-nnfbd0

Description: If two formulas are equivalent, then nonfreeness of a variable in one of them is equivalent to nonfreeness in the other, deduction form. The antecedent of the conclusion is in the "strong necessity" modality of modal logic (see also bj-nnftht ) in order not to require sp (modal T). See bj-nnfbi . (Contributed by BJ, 21-Mar-2026)

	Ref	Expression
Hypothesis	bj-nnfbd0.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
Assertion	bj-nnfbd0	$$⊢\left(\phi \wedge \forall x\phi \right)\to \left(Ⅎ\text{'}x\psi \leftrightarrow Ⅎ\text{'}x\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-nnfbd0.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
2	1	alimi	$$⊢\forall x\phi \to \forall x\left(\psi \leftrightarrow \chi \right)$$
3		bj-nnfbi	$$⊢\left(\left(\psi \leftrightarrow \chi \right)\wedge \forall x\left(\psi \leftrightarrow \chi \right)\right)\to \left(Ⅎ\text{'}x\psi \leftrightarrow Ⅎ\text{'}x\chi \right)$$
4	1 2 3	syl2an	$$⊢\left(\phi \wedge \forall x\phi \right)\to \left(Ⅎ\text{'}x\psi \leftrightarrow Ⅎ\text{'}x\chi \right)$$