Theorem nfxfrd 1930

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 1928	. 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
4	1, 3	sylibr 224	1 ⊢ (𝜒 → Ⅎ𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 196  Ⅎwnf 1856

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

This theorem depends on definitions:  df-bi 197  df-ex 1853  df-nf 1858

This theorem is referenced by:  nfand  1978  nf3and  1979  nfbid  1984  nfexd  2329  dvelimhw  2338  nfexd2  2482  dvelimf  2484  nfeud2  2630  nfmod2  2631  nfeqd  2921  nfeld  2922  nfabd2  2933  nfned  3044  nfneld  3054  nfrald  3093  nfrexd  3154  nfreud  3260  nfrmod  3261  nfsbc1d  3606  nfsbcd  3609  nfbrd  4833  bj-dvelimdv  33169  wl-nfnbi  33650  wl-sb8eut  33694