Theorem nfxfrd 1404

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

Syntax hints:   -> wi 4   <-> wb 103   F/wnf 1389

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378

This theorem depends on definitions:  df-bi 115  df-nf 1390

This theorem is referenced by:  nf3and  1501  nfbid  1520  nfsbxy  1859  nfsbxyt  1860  nfeud  1957  nfmod  1958  nfeqd  2233  nfeld  2234  nfabd  2237  nfned  2338  nfneld  2347  nfraldxy  2398  nfrexdxy  2399  nfraldya  2400  nfrexdya  2401  nfsbc1d  2831  nfsbcd  2834  nfbrd  3828