Theorem bj-nnfbd0 37489

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 37484) in order not to require sp 2221 (modal T). See bj-nnfbi 37488. (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 1844	. 2 ⊢ (∀𝑥𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		bj-nnfbi 37488	. 2 ⊢ (((𝜓 ↔ 𝜒) ∧ ∀𝑥(𝜓 ↔ 𝜒)) → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒))
4	1, 2, 3	syl2an 608	1 ⊢ ((𝜑 ∧ ∀𝑥𝜑) → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568  Ⅎ'wnnf 37467

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-bj-nnf 37468

This theorem is used by:  bj-nnfbd  37510