Theorem nfxfrd 1626

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

Syntax hints:   -> wi 4   <-> wb 184   F/wnf 1599

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

This theorem depends on definitions:  df-bi 185  df-nf 1600

This theorem is referenced by:  nfand  1872  nf3and  1873  nfbid  1880  nfexd  1899  dvelimhw  1902  nfexd2  2047  dvelimf  2049  nfeud2  2290  nfmod2  2291  nfeud2OLD  2302  nfeqd  2636  nfeld  2637  nfabd2  2650  nfned  2799  nfneld  2811  nfrald  2852  nfrexd  2929  nfreud  3039  nfrmod  3040  nfsbc1d  3354  nfsbcd  3357  nfbrd  4496  wl-sb8eut  29949