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  2330  dvelimhw  2345  nfexd2  2446  dvelimf  2448  nfmod2  2553  nfmodv  2554  nfeud2  2585  nfeudw  2586  nfeqd  2905  nfeld  2906  nfabdw  2916  nfabd  2917  nfned  3030  nfneld  3041  nfraldw  3277  nfrexdw  3278  nfrald  3338  nfrexd  3339  nfrmod  3391  nfreud  3392  nfsbc1d  3759  nfsbcdw  3762  nfsbcd  3765  nfbrd  5137  nfchnd  18514  bj-dvelimdv  36884  bj-nfexd  37171  wl-sb8eut  37611  wl-sb8eutv  37612