Theorem nf5rd 2198

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 2195	. 2 ⊢ (Ⅎ𝑥𝜓 → (𝜓 → ∀𝑥𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-12 2179

This theorem depends on definitions:  df-bi 210  df-ex 1787  df-nf 1791

This theorem is referenced by:  spimedv  2199  alrimdd  2216  nf5di  2289  hbnt  2298  hbimd  2302  dvelimhw  2348  dveeq2  2378  dveeq1  2380  axc9  2382  spimed  2388  dvelimh  2450  abidnf  3602  eusvnfb  5260  axrepnd  10094  axacndlem4  10110  bj-cbv2v  34623  bj-elgab  34770  wl-nfeqfb  35338