Theorem nfxfrd 1852

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

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

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

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782

This theorem is referenced by:  nfand  1896  nf3and  1897  nfbid  1901  nfexd  2333  dvelimhw  2351  nfexd2  2454  dvelimf  2456  nfmod2  2561  nfmodv  2562  nfeud2  2593  nfeudw  2594  nfeqd  2919  nfeld  2920  nfabdw  2932  nfabdwOLD  2933  nfabd  2934  nfned  3050  nfneld  3061  nfraldw  3315  nfrexdw  3316  nfraldwOLD  3328  nfrald  3380  nfrexd  3381  nfreuwOLD  3433  nfrmod  3439  nfreud  3440  nfsbc1d  3822  nfsbcdw  3825  nfsbcd  3828  nfbrd  5212  bj-dvelimdv  36817  bj-nfexd  37104  wl-sb8eut  37532  wl-sb8eutv  37533