Theorem nfxfrd 1855

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

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

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

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfand  1898  nf3and  1899  nfbid  1903  nfexd  2334  dvelimhw  2349  nfexd2  2450  dvelimf  2452  nfmod2  2558  nfmodv  2559  nfeud2  2590  nfeudw  2591  nfeqd  2909  nfeld  2910  nfabdw  2920  nfabd  2921  nfned  3034  nfneld  3045  nfraldw  3281  nfrexdw  3282  nfrald  3342  nfrexd  3343  nfrmod  3395  nfreud  3396  nfsbc1d  3758  nfsbcdw  3761  nfsbcd  3764  nfbrd  5144  nfchnd  18534  bj-dvelimdv  37052  bj-nfexd  37339  wl-sb8eut  37779  wl-sb8eutv  37780