Theorem nfxfrd 1873

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

Syntax hints:   → wi 4   ↔ wb 208  Ⅎwnf 1802

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

This theorem depends on definitions:  df-bi 209  df-ex 1799  df-nf 1803

This theorem is referenced by:  nfand  1916  nf3and  1917  nfbid  1921  nfexd  2360  dvelimhw  2375  nfexd2  2476  dvelimf  2478  nfmod2  2584  nfmodv  2585  nfeud2  2616  nfeudw  2617  nfeqd  2933  nfeld  2934  nfabdw  2944  nfabd  2945  nfned  3058  nfneld  3069  nfraldw  3306  nfrexdw  3307  nfrald  3358  nfrexd  3359  nfrmod  3409  nfreud  3410  nfsbc1d  3762  nfsbcdw  3765  nfsbcd  3768  nfbrd  5145  nfchnd  18626  bj-dvelimdv  37300  bj-nfexd  37592  wl-sb8eut  38045  wl-sb8eutv  38046