Theorem nfxfrd 1475

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 1473	. 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 1460

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 1447  ax-gen 1449

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

This theorem is referenced by:  nf3and  1569  nfbid  1588  nfsbxy  1942  nfsbxyt  1943  nfeud  2042  nfmod  2043  nfeqd  2334  nfeld  2335  nfabdw  2338  nfabd  2339  nfned  2441  nfneld  2450  nfraldw  2509  nfraldxy  2510  nfrexdxy  2511  nfraldya  2512  nfrexdya  2513  nfsbc1d  2980  nfsbcd  2983  nfsbcdw  3092  nfbrd  4049