Theorem nfxfrd 1855

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

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

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

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfand  1898  nf3and  1899  nfbid  1903  nfexd  2332  dvelimhw  2347  nfexd2  2448  dvelimf  2450  nfmod2  2555  nfmodv  2556  nfeud2  2587  nfeudw  2588  nfeqd  2906  nfeld  2907  nfabdw  2917  nfabd  2918  nfned  3031  nfneld  3042  nfraldw  3278  nfrexdw  3279  nfrald  3339  nfrexd  3340  nfrmod  3392  nfreud  3393  nfsbc1d  3755  nfsbcdw  3758  nfsbcd  3761  nfbrd  5139  nfchnd  18519  bj-dvelimdv  36916  bj-nfexd  37203  wl-sb8eut  37643  wl-sb8eutv  37644