Theorem nfxfrd 1848

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

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1777

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

This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778

This theorem is referenced by:  nfand  1892  nf3and  1893  nfbid  1897  nfexd  2317  dvelimhw  2336  nfexd2  2440  dvelimf  2442  nfmod2  2547  nfmodv  2548  nfeud2  2579  nfeudw  2580  nfeqd  2910  nfeld  2911  nfabdw  2923  nfabdwOLD  2924  nfabd  2925  nfned  3041  nfneld  3052  nfraldw  3304  nfrexdw  3305  nfraldwOLD  3316  nfrald  3366  nfrexd  3367  nfreuwOLD  3420  nfrmod  3426  nfreud  3427  nfsbc1d  3796  nfsbcdw  3799  nfsbcd  3802  nfbrd  5198  bj-dvelimdv  36361  bj-nfexd  36650  wl-sb8eut  37078  wl-sb8eutv  37079