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  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  3282  nfrexdw  3283  nfrald  3334  nfrexd  3335  nfrmod  3385  nfreud  3386  nfsbc1d  3746  nfsbcdw  3749  nfsbcd  3752  nfbrd  5131  nfchnd  18577  bj-dvelimdv  37158  bj-nfexd  37450  wl-sb8eut  37903  wl-sb8eutv  37904