Theorem nf5rd 2233

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  spimedv  2234  alrimdd  2251  nf5di  2319  hbnt  2328  hbimd  2332  dvelimhw  2375  dveeq2  2408  dveeq1  2410  axc9  2412  spimed  2418  dvelimh  2480  abidnf  3660  eusvnfb  5355  axrepnd  10679  axacndlem4  10695  bj-cbv2v  37710  bj-elgab  37852  wl-nfeqfb  38468