Theorem nfxfrd 1499

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

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

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 1471  ax-gen 1473

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

This theorem is referenced by:  nf3and  1593  nfbid  1612  nfsbxy  1971  nfsbxyt  1972  nfeud  2071  nfmod  2072  nfeqd  2364  nfeld  2365  nfabdw  2368  nfabd  2369  nfned  2471  nfneld  2480  nfraldw  2539  nfraldxy  2540  nfrexdxy  2541  nfraldya  2542  nfrexdya  2543  nfsbc1d  3017  nfsbcd  3020  nfsbcdw  3129  nfbrd  4094