Theorem nfxfrd 1499

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 1497	. 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 1484

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 1471  ax-gen 1473

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

This theorem is referenced by:  nf3and  1593  nfbid  1612  nfsbxy  1971  nfsbxyt  1972  nfeud  2071  nfmod  2072  nfeqd  2365  nfeld  2366  nfabdw  2369  nfabd  2370  nfned  2472  nfneld  2481  nfraldw  2540  nfraldxy  2541  nfrexdxy  2542  nfraldya  2543  nfrexdya  2544  nfsbc1d  3022  nfsbcd  3025  nfsbcdw  3135  nfbrd  4105