Theorem nf5rd 2195

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

Hypothesis

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

Assertion

Ref	Expression
nf5rd	⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))

Proof of Theorem nf5rd

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

Syntax hints:   → wi 4  ∀wal 1537  Ⅎwnf 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-ex 1779  df-nf 1783

This theorem is referenced by:  spimedv  2196  alrimdd  2213  nf5di  2284  hbnt  2293  hbimd  2297  dvelimhw  2346  dveeq2  2382  dveeq1  2384  axc9  2386  spimed  2392  dvelimh  2454  abidnf  3707  eusvnfb  5392  axrepnd  10635  axacndlem4  10651  bj-cbv2v  36800  bj-elgab  36941  wl-nfeqfb  37538