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  2329  dvelimhw  2346  nfexd2  2450  dvelimf  2452  nfmod2  2557  nfmodv  2558  nfeud2  2589  nfeudw  2590  nfeqd  2909  nfeld  2910  nfabdw  2920  nfabd  2921  nfned  3034  nfneld  3045  nfraldw  3289  nfrexdw  3290  nfrald  3351  nfrexd  3352  nfreuwOLD  3405  nfrmod  3411  nfreud  3412  nfsbc1d  3783  nfsbcdw  3786  nfsbcd  3789  nfbrd  5165  bj-dvelimdv  36815  bj-nfexd  37102  wl-sb8eut  37542  wl-sb8eutv  37543