Theorem bj-nnfbd0 37187

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 37182) in order not to require sp 2217 (modal T). See bj-nnfbi 37186. (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 1830	. 2 ⊢ (∀𝑥𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		bj-nnfbi 37186	. 2 ⊢ (((𝜓 ↔ 𝜒) ∧ ∀𝑥(𝜓 ↔ 𝜒)) → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒))
4	1, 2, 3	syl2an 605	1 ⊢ ((𝜑 ∧ ∀𝑥𝜑) → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1557  Ⅎ'wnnf 37165

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-bj-nnf 37166

This theorem is referenced by:  bj-nnfbd  37208