Theorem bj-nnfbd0 37841

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

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

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 37820

This theorem is used by:  bj-nnfbd  37862