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  1996  nfsbxyt  1997  nfeud  2096  nfmod  2097  nfeqd  2399  nfeld  2400  nfabdw  2403  nfabd  2404  nfned  2506  nfneld  2515  nfraldw  2574  nfraldxy  2575  nfrexdxy  2576  nfraldya  2577  nfrexdya  2578  nfsbc1d  3059  nfsbcd  3062  nfsbcdw  3172  nfbrd  4155