Theorem nf5rd 2232

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816

This theorem is used by:  spimedv  2233  alrimdd  2250  nf5di  2318  hbnt  2327  hbimd  2331  dvelimhw  2374  dveeq2  2407  dveeq1  2409  axc9  2411  spimed  2417  dvelimh  2479  abidnf  3659  eusvnfb  5355  axrepnd  10686  axacndlem4  10702  bj-cbv2v  37834  bj-elgab  37976  wl-nfeqfb  38605