Theorem nfxfrd 1524

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 1522	. 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 1509

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 1496  ax-gen 1498

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

This theorem is referenced by:  nf3and  1618  nfbid  1637  nfsbxy  1995  nfsbxyt  1996  nfeud  2095  nfmod  2096  nfeqd  2390  nfeld  2391  nfabdw  2394  nfabd  2395  nfned  2497  nfneld  2506  nfraldw  2565  nfraldxy  2566  nfrexdxy  2567  nfraldya  2568  nfrexdya  2569  nfsbc1d  3049  nfsbcd  3052  nfsbcdw  3162  nfbrd  4139