Theorem nfxfrd 1772

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

Syntax hints:   → wi 4   ↔ wb 195  Ⅎwnf 1699

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

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701

This theorem is referenced by:  nfand  1814  nf3and  1815  nfbid  1820  nfexd  2153  dvelimhw  2159  nfexd2  2320  dvelimf  2322  nfeud2  2470  nfmod2  2471  nfeqd  2758  nfeld  2759  nfabd2  2770  nfned  2883  nfneld  2891  nfrald  2928  nfrexd  2989  nfreud  3091  nfrmod  3092  nfsbc1d  3420  nfsbcd  3423  nfbrd  4628  bj-dvelimdv  32027  wl-nfnbi  32493  wl-sb8eut  32538