Theorem nfxfrd 1364

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

Syntax hints:   -> wi 4   <-> wb 98   F/wnf 1349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338

This theorem depends on definitions:  df-bi 110  df-nf 1350

This theorem is referenced by:  nf3and  1461  nfbid  1480  nfsbxy  1818  nfsbxyt  1819  nfeud  1916  nfmod  1917  nfeqd  2192  nfeld  2193  nfabd  2196  nfned  2298  nfneld  2305  nfraldxy  2356  nfrexdxy  2357  nfraldya  2358  nfrexdya  2359  nfsbc1d  2780  nfsbcd  2783  nfbrd  3807