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  3335  nfrexd  3336  nfrmod  3386  nfreud  3387  nfsbc1d  3747  nfsbcdw  3750  nfsbcd  3753  nfbrd  5132  nfchnd  18568  bj-dvelimdv  37174  bj-nfexd  37466  wl-sb8eut  37917  wl-sb8eutv  37918