Theorem nfxfrd 1528

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

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502

This theorem depends on definitions:  df-bi 117  df-nf 1514

This theorem is referenced by:  nf3and  1622  nfbid  1641  nfsbxy  2002  nfsbxyt  2003  nfeud  2102  nfmod  2103  nfeqd  2407  nfeld  2408  nfabdw  2411  nfabd  2412  nfned  2514  nfneld  2523  nfraldw  2582  nfraldxy  2583  nfrexdxy  2584  nfraldya  2585  nfrexdya  2586  nfsbc1d  3068  nfsbcd  3071  nfsbcdw  3181  nfbrd  4174