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	$$⊢\forall x\phi \to \left(Ⅎx\left(\phi \to \psi \right)\leftrightarrow Ⅎx\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfa1	$$⊢Ⅎx\forall x\phi$$
2		pm5.5	$$⊢\phi \to \left(\left(\phi \to \psi \right)\leftrightarrow \psi \right)$$
3	2	sps	$$⊢\forall x\phi \to \left(\left(\phi \to \psi \right)\leftrightarrow \psi \right)$$
4	1 3	nfbidf	$$⊢\forall x\phi \to \left(Ⅎx\left(\phi \to \psi \right)\leftrightarrow Ⅎx\psi \right)$$