Theorem nfxfrd 1856

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	⊢ (𝜑 ↔ 𝜓)
nfxfrd.2	⊢ (𝜒 → Ⅎ𝑥𝜓)

Assertion

Ref	Expression
nfxfrd	⊢ (𝜒 → Ⅎ𝑥𝜑)

Proof of Theorem nfxfrd

Step	Hyp	Ref	Expression
1		nfxfrd.2	. 2 ⊢ (𝜒 → Ⅎ𝑥𝜓)
2		nfbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	nfbii 1854	. 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
4	1, 3	sylibr 234	1 ⊢ (𝜒 → Ⅎ𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfand  1899  nf3and  1900  nfbid  1904  nfexd  2335  dvelimhw  2350  nfexd2  2451  dvelimf  2453  nfmod2  2559  nfmodv  2560  nfeud2  2591  nfeudw  2592  nfeqd  2910  nfeld  2911  nfabdw  2921  nfabd  2922  nfned  3035  nfneld  3046  nfraldw  3283  nfrexdw  3284  nfrald  3344  nfrexd  3345  nfrmod  3397  nfreud  3398  nfsbc1d  3760  nfsbcdw  3763  nfsbcd  3766  nfbrd  5146  nfchnd  18546  bj-dvelimdv  37096  bj-nfexd  37388  wl-sb8eut  37830  wl-sb8eutv  37831