Theorem nfxfrd 1498

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

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 1470  ax-gen 1472

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

This theorem is referenced by:  nf3and  1592  nfbid  1611  nfsbxy  1970  nfsbxyt  1971  nfeud  2070  nfmod  2071  nfeqd  2363  nfeld  2364  nfabdw  2367  nfabd  2368  nfned  2470  nfneld  2479  nfraldw  2538  nfraldxy  2539  nfrexdxy  2540  nfraldya  2541  nfrexdya  2542  nfsbc1d  3015  nfsbcd  3018  nfsbcdw  3127  nfbrd  4089