Theorem nfxfrd 1463

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

Syntax hints:   -> wi 4   <-> wb 104   F/wnf 1448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437

This theorem depends on definitions:  df-bi 116  df-nf 1449

This theorem is referenced by:  nf3and  1557  nfbid  1576  nfsbxy  1930  nfsbxyt  1931  nfeud  2030  nfmod  2031  nfeqd  2323  nfeld  2324  nfabdw  2327  nfabd  2328  nfned  2430  nfneld  2439  nfraldw  2498  nfraldxy  2499  nfrexdxy  2500  nfraldya  2501  nfrexdya  2502  nfsbc1d  2967  nfsbcd  2970  nfsbcdw  3079  nfbrd  4027