Theorem nf5rd 2104

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

Syntax hints:   → wi 4  ∀wal 1521  Ⅎwnf 1748

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087

This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750

This theorem is referenced by:  alrimdd  2121  nf5di  2157  hbimd  2164  hbnt  2182  nfaldOLD  2202  dvelimhw  2209  spimed  2291  cbv2  2306  dveeq2  2334  dveeq1  2336  axc9  2338  dvelimh  2367  abidnf  3408  eusvnfb  4892  axrepnd  9454  axacndlem4  9470  bj-spimedv  32844  bj-cbv2v  32857  wl-nfeqfb  33453