Theorem nfxfrd 1877

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

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1806

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

This theorem depends on definitions:  df-bi 210  df-ex 1803  df-nf 1807

This theorem is referenced by:  nfand  1920  nf3and  1921  nfbid  1925  nfexd  2364  dvelimhw  2379  nfexd2  2480  dvelimf  2482  nfmod2  2588  nfmodv  2589  nfeud2  2620  nfeudw  2621  nfeqd  2937  nfeld  2938  nfabdw  2948  nfabd  2949  nfned  3062  nfneld  3073  nfraldw  3310  nfrexdw  3311  nfrald  3362  nfrexd  3363  nfrmod  3413  nfreud  3414  nfsbc1d  3765  nfsbcdw  3768  nfsbcd  3771  nfbrd  5151  nfchnd  18657  bj-dvelimdv  37348  bj-nfexd  37640  wl-sb8eut  38093  wl-sb8eutv  38094