Theorem nfxfrd 1497

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

Syntax hints:   -> wi 4   <-> wb 105   F/wnf 1482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471

This theorem depends on definitions:  df-bi 117  df-nf 1483

This theorem is referenced by:  nf3and  1591  nfbid  1610  nfsbxy  1969  nfsbxyt  1970  nfeud  2069  nfmod  2070  nfeqd  2362  nfeld  2363  nfabdw  2366  nfabd  2367  nfned  2469  nfneld  2478  nfraldw  2537  nfraldxy  2538  nfrexdxy  2539  nfraldya  2540  nfrexdya  2541  nfsbc1d  3014  nfsbcd  3017  nfsbcdw  3126  nfbrd  4088