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

Metamath Proof Explorer

Theorem nf5rd

Description: Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016)

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

Proof

Step Hyp Ref Expression
1 nf5rd.1 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
2 nf5r ⊢ ( Ⅎ 𝑥 𝜓 → ( 𝜓 → ∀ 𝑥 𝜓 ) )
3 1 2 syl ⊢ ( 𝜑 → ( 𝜓 → ∀ 𝑥 𝜓 ) )