Theorem nfxfrd 1468

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 1466	. 2 |- ( F/ x ph <-> F/ x ps )
4	1, 3	sylibr 133	1 |- ( ch -> F/ x ph )

Syntax hints:   -> wi 4   <-> wb 104   F/wnf 1453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442

This theorem depends on definitions:  df-bi 116  df-nf 1454

This theorem is referenced by:  nf3and  1562  nfbid  1581  nfsbxy  1935  nfsbxyt  1936  nfeud  2035  nfmod  2036  nfeqd  2327  nfeld  2328  nfabdw  2331  nfabd  2332  nfned  2434  nfneld  2443  nfraldw  2502  nfraldxy  2503  nfrexdxy  2504  nfraldya  2505  nfrexdya  2506  nfsbc1d  2971  nfsbcd  2974  nfsbcdw  3083  nfbrd  4034