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-mp 5  ax-1 6  ax-2 7  ax-3 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  2504  nfeld  2505  nfabd2  2508  nfned  2613  nfneld  2614  nfrald  2666  nfrexd  2667  nfreud  2784  nfrmod  2785  nfsbc1d  3064  nfsbcd  3067  nfbrd  4683