Theorem nfxfrd 1694

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 1692	. 2 |- ( F/ x ph <-> F/ x ps )
4	1, 3	sylibr 216	1 |- ( ch -> F/ x ph )

Syntax hints:   -> wi 4   <-> wb 188   F/wnf 1664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679

This theorem depends on definitions:  df-bi 189  df-nf 1665

This theorem is referenced by:  nfand  1982  nf3and  1983  nfbid  1990  nfexd  2009  dvelimhw  2012  nfexd2  2130  dvelimf  2132  nfeud2  2279  nfmod2  2280  nfeqd  2592  nfeld  2593  nfabd2  2606  nfned  2758  nfneld  2770  nfrald  2811  nfrexd  2888  nfreud  3002  nfrmod  3003  nfsbc1d  3318  nfsbcd  3321  nfbrd  4465  wl-nfnbi  31779  wl-sb8eut  31826