Theorem wl-nfimf1

Description: An antecedent is irrelevant to a not-free property, if it always holds. I used this variant of nfim in dvelimdf to simplify the proof. (Contributed by Wolf Lammen, 14-Oct-2018)

	Ref	Expression
Assertion	wl-nfimf1	⊢ ( ∀ 𝑥 𝜑 → ( Ⅎ 𝑥 ( 𝜑 → 𝜓 ) ↔ Ⅎ 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 𝜑
2		pm5.5	⊢ ( 𝜑 → ( ( 𝜑 → 𝜓 ) ↔ 𝜓 ) )
3	2	sps	⊢ ( ∀ 𝑥 𝜑 → ( ( 𝜑 → 𝜓 ) ↔ 𝜓 ) )
4	1 3	nfbidf	⊢ ( ∀ 𝑥 𝜑 → ( Ⅎ 𝑥 ( 𝜑 → 𝜓 ) ↔ Ⅎ 𝑥 𝜓 ) )