Theorem nfxfrd 1485

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 1483	. 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 1470

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 1457  ax-gen 1459

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

This theorem is referenced by:  nf3and  1579  nfbid  1598  nfsbxy  1953  nfsbxyt  1954  nfeud  2053  nfmod  2054  nfeqd  2346  nfeld  2347  nfabdw  2350  nfabd  2351  nfned  2453  nfneld  2462  nfraldw  2521  nfraldxy  2522  nfrexdxy  2523  nfraldya  2524  nfrexdya  2525  nfsbc1d  2993  nfsbcd  2996  nfsbcdw  3105  nfbrd  4062