Theorem nf5rd 2231

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

Syntax hints:   → wi 4  ∀wal 1558  Ⅎwnf 1803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-12 2212

This theorem depends on definitions:  df-bi 209  df-ex 1800  df-nf 1804

This theorem is referenced by:  spimedv  2232  alrimdd  2249  nf5di  2319  hbnt  2328  hbimd  2332  dvelimhw  2376  dveeq2  2409  dveeq1  2411  axc9  2413  spimed  2419  dvelimh  2481  abidnf  3665  eusvnfb  5350  axrepnd  10552  axacndlem4  10568  bj-cbv2v  37283  bj-elgab  37424  wl-nfeqfb  38039