Theorem nfxfrd 1486

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

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 1458  ax-gen 1460

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

This theorem is referenced by:  nf3and  1580  nfbid  1599  nfsbxy  1958  nfsbxyt  1959  nfeud  2058  nfmod  2059  nfeqd  2351  nfeld  2352  nfabdw  2355  nfabd  2356  nfned  2458  nfneld  2467  nfraldw  2526  nfraldxy  2527  nfrexdxy  2528  nfraldya  2529  nfrexdya  2530  nfsbc1d  3002  nfsbcd  3005  nfsbcdw  3114  nfbrd  4074