Theorem bj-nnfbd0 37098

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1545  Ⅎ'wnnf 37076

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-bj-nnf 37077

This theorem is referenced by:  bj-nnfbd  37119