Theorem nfxfrd 1524

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

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

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 1496  ax-gen 1498

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

This theorem is referenced by:  nf3and  1618  nfbid  1637  nfsbxy  1998  nfsbxyt  1999  nfeud  2098  nfmod  2099  nfeqd  2401  nfeld  2402  nfabdw  2405  nfabd  2406  nfned  2508  nfneld  2517  nfraldw  2576  nfraldxy  2577  nfrexdxy  2578  nfraldya  2579  nfrexdya  2580  nfsbc1d  3062  nfsbcd  3065  nfsbcdw  3175  nfbrd  4160