Theorem nf5rd 2066

Description: Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nf5rd.1	|- ( ph -> F/ x ps )

Assertion

Ref	Expression
nf5rd	|- ( ph -> ( ps -> A. x ps ) )

Proof of Theorem nf5rd

Step	Hyp	Ref	Expression
1		nf5rd.1	. 2 |- ( ph -> F/ x ps )
2		nf5r 2064	. 2 |- ( F/ x ps -> ( ps -> A. x ps ) )
3	1, 2	syl 17	1 |- ( ph -> ( ps -> A. x ps ) )

Syntax hints:   -> wi 4   A.wal 1481   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710

This theorem is referenced by:  alrimdd  2083  nf5di  2119  hbimd  2126  hbnt  2144  nfaldOLD  2166  dvelimhw  2173  spimed  2255  cbv2  2270  dveeq2  2298  dveeq1  2300  axc9  2302  dvelimh  2336  abidnf  3375  eusvnfb  4862  axrepnd  9416  axacndlem4  9432  bj-spimedv  32719  bj-cbv2v  32732  wl-nfeqfb  33323