Theorem bj-nnfbd0 37235

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 37230) in order not to require sp 2221 (modal T). See bj-nnfbi 37234. (Contributed by BJ, 21-Mar-2026.)

Hypothesis

Ref	Expression
bj-nnfbd0.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
bj-nnfbd0	⊢ ((𝜑 ∧ ∀𝑥𝜑) → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒))

Proof of Theorem bj-nnfbd0

Step	Hyp	Ref	Expression
1		bj-nnfbd0.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	alimi 1834	. 2 ⊢ (∀𝑥𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		bj-nnfbi 37234	. 2 ⊢ (((𝜓 ↔ 𝜒) ∧ ∀𝑥(𝜓 ↔ 𝜒)) → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒))
4	1, 2, 3	syl2an 607	1 ⊢ ((𝜑 ∧ ∀𝑥𝜑) → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1561  Ⅎ'wnnf 37213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-bj-nnf 37214

This theorem is referenced by:  bj-nnfbd  37256