Theorem nfxfrd 1861

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

Syntax hints:   → wi 4   ↔ wb 207  Ⅎwnf 1790

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

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-nf 1791

This theorem is referenced by:  nfand  1904  nf3and  1905  nfbid  1909  nfexd  2338  dvelimhw  2353  nfexd2  2454  dvelimf  2456  nfmod2  2562  nfmodv  2563  nfeud2  2594  nfeudw  2595  nfeqd  2912  nfeld  2913  nfabdw  2923  nfabd  2924  nfned  3037  nfneld  3048  nfraldw  3285  nfrexdw  3286  nfrald  3337  nfrexd  3338  nfrmod  3388  nfreud  3389  nfsbc1d  3748  nfsbcdw  3751  nfsbcd  3754  nfbrd  5125  nfchnd  18575  bj-dvelimdv  37211  bj-nfexd  37503  wl-sb8eut  37956  wl-sb8eutv  37957