Theorem nfxfrd 1571

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses

Ref	Expression
nfbii.1	|- (ph <-> ps)
nfxfrd.2	|- (ch -> F/xps)

Assertion

Ref	Expression
nfxfrd	|- (ch -> F/xph)

Proof of Theorem nfxfrd

Step	Hyp	Ref	Expression
1		nfxfrd.2	. 2 |- (ch -> F/xps)
2		nfbii.1	. . 3 |- (ph <-> ps)
3	2	nfbii 1569	. 2 |- ( F/xph <-> F/xps)
4	1, 3	sylibr 203	1 |- (ch -> F/xph)

Syntax hints:   -> wi 4   <-> wb 176   F/wnf 1544

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557

This theorem depends on definitions:  df-bi 177  df-nf 1545

This theorem is referenced by:  nfand  1822  nf3and  1823  nfbid  1832  nfbidOLD  1833  nfexd  1854  nfexd2  1973  dvelimf  1997  nfeud2  2216  nfmod2  2217  nfeqd  2503  nfeld  2504  nfabd2  2507  nfned  2612  nfneld  2613  nfrald  2665  nfrexd  2666  nfreud  2783  nfrmod  2784  nfsbc1d  3063  nfsbcd  3066  nfbrd  4682