This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfd

Description: Deduce that x is not free in ps in a context. (Contributed by Wolf Lammen, 16-Sep-2021)

Ref Expression
Hypothesis nfd.1 ⊢ ( 𝜑 → ( ∃ 𝑥 𝜓 → ∀ 𝑥 𝜓 ) )
Assertion nfd ( 𝜑 → Ⅎ 𝑥 𝜓 )

Proof

Step Hyp Ref Expression
1 nfd.1 ⊢ ( 𝜑 → ( ∃ 𝑥 𝜓 → ∀ 𝑥 𝜓 ) )
2 df-nf ⊢ ( Ⅎ 𝑥 𝜓 ↔ ( ∃ 𝑥 𝜓 → ∀ 𝑥 𝜓 ) )
3 1 2 sylibr ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )