Theorem nfxfrd 1854

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

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

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

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfand  1897  nf3and  1898  nfbid  1902  nfexd  2328  dvelimhw  2343  nfexd2  2444  dvelimf  2446  nfmod2  2551  nfmodv  2552  nfeud2  2583  nfeudw  2584  nfeqd  2902  nfeld  2903  nfabdw  2913  nfabd  2914  nfned  3027  nfneld  3038  nfraldw  3283  nfrexdw  3284  nfrald  3346  nfrexd  3347  nfrmod  3401  nfreud  3402  nfsbc1d  3771  nfsbcdw  3774  nfsbcd  3777  nfbrd  5153  bj-dvelimdv  36839  bj-nfexd  37126  wl-sb8eut  37566  wl-sb8eutv  37567