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  1996  nfsbxyt  1997  nfeud  2096  nfmod  2097  nfeqd  2399  nfeld  2400  nfabdw  2403  nfabd  2404  nfned  2506  nfneld  2515  nfraldw  2574  nfraldxy  2575  nfrexdxy  2576  nfraldya  2577  nfrexdya  2578  nfsbc1d  3058  nfsbcd  3061  nfsbcdw  3171  nfbrd  4154