Theorem nfxfrd 1452

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 1450	. 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 1437

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 1424  ax-gen 1426

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

This theorem is referenced by:  nf3and  1549  nfbid  1568  nfsbxy  1916  nfsbxyt  1917  nfeud  2016  nfmod  2017  nfeqd  2297  nfeld  2298  nfabd  2301  nfned  2403  nfneld  2412  nfraldxy  2470  nfrexdxy  2471  nfraldya  2472  nfrexdya  2473  nfsbc1d  2929  nfsbcd  2932  nfbrd  3981