Metamath Proof Explorer
Theorem nfd
Description: Deduce that x is not free in ps in a context. (Contributed by Wolf Lammen, 16Sep2021)


Ref 
Expression 

Hypothesis 
nfd.1 
⊢ ( 𝜑 → ( ∃ 𝑥 𝜓 → ∀ 𝑥 𝜓 ) ) 

Assertion 
nfd 
⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

nfd.1 
⊢ ( 𝜑 → ( ∃ 𝑥 𝜓 → ∀ 𝑥 𝜓 ) ) 
2 

dfnf 
⊢ ( Ⅎ 𝑥 𝜓 ↔ ( ∃ 𝑥 𝜓 → ∀ 𝑥 𝜓 ) ) 
3 
1 2

sylibr 
⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 ) 