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 233	1 ⊢ (𝜒 → Ⅎ𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 205  Ⅎ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 206  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfand  1900  nf3and  1901  nfbid  1905  nfexd  2322  dvelimhw  2341  nfexd2  2444  dvelimf  2446  nfmod2  2551  nfmodv  2552  nfeud2  2583  nfeudw  2584  nfeqd  2912  nfeld  2913  nfabdw  2925  nfabdwOLD  2926  nfabd  2927  nfned  3043  nfneld  3054  nfraldw  3290  nfrexdw  3291  nfraldwOLD  3300  nfrald  3343  nfrexd  3344  nfreuwOLD  3395  nfrmod  3401  nfreud  3402  nfsbc1d  3760  nfsbcdw  3763  nfsbcd  3766  nfbrd  5156  bj-dvelimdv  35393  bj-nfexd  35682  wl-sb8eut  36105