Theorem nfxfrd 1523

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 1521	. 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 1508

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 1495  ax-gen 1497

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

This theorem is referenced by:  nf3and  1617  nfbid  1636  nfsbxy  1995  nfsbxyt  1996  nfeud  2095  nfmod  2096  nfeqd  2389  nfeld  2390  nfabdw  2393  nfabd  2394  nfned  2496  nfneld  2505  nfraldw  2564  nfraldxy  2565  nfrexdxy  2566  nfraldya  2567  nfrexdya  2568  nfsbc1d  3048  nfsbcd  3051  nfsbcdw  3161  nfbrd  4134