Theorem nfxfrd 1780

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/ x ps )

Assertion

Ref	Expression
nfxfrd	|- ( ch -> F/ x ph )

Proof of Theorem nfxfrd

Step	Hyp	Ref	Expression
1		nfxfrd.2	. 2 |- ( ch -> F/ x ps )
2		nfbii.1	. . 3 |- ( ph <-> ps )
3	2	nfbii 1778	. 2 |- ( F/ x ph <-> F/ x ps )
4	1, 3	sylibr 224	1 |- ( ch -> F/ x ph )

Syntax hints:   -> wi 4   <-> wb 196   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

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

This theorem is referenced by:  nfand  1826  nf3and  1827  nfbid  1832  nfexd  2167  dvelimhw  2173  nfexd2  2332  dvelimf  2334  nfeud2  2482  nfmod2  2483  nfeqd  2772  nfeld  2773  nfabd2  2784  nfned  2895  nfneld  2905  nfrald  2944  nfrexd  3006  nfreud  3112  nfrmod  3113  nfsbc1d  3453  nfsbcd  3456  nfbrd  4698  bj-dvelimdv  32834  wl-nfnbi  33314  wl-sb8eut  33359