Theorem nf5rd 2190

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  spimedv  2191  alrimdd  2208  nf5di  2282  hbnt  2291  hbimd  2295  dvelimhw  2342  dveeq2  2378  dveeq1  2380  axc9  2382  spimed  2388  dvelimh  2450  abidnf  3698  eusvnfb  5391  axrepnd  10586  axacndlem4  10602  bj-cbv2v  35665  bj-elgab  35808  wl-nfeqfb  36394