ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfxfrd GIF version

Theorem nfxfrd 1436
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
StepHypRef Expression
1 nfxfrd.2 . 2 (𝜒 → Ⅎ𝑥𝜓)
2 nfbii.1 . . 3 (𝜑𝜓)
32nfbii 1434 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3sylibr 133 1 (𝜒 → Ⅎ𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wnf 1421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410
This theorem depends on definitions:  df-bi 116  df-nf 1422
This theorem is referenced by:  nf3and  1533  nfbid  1552  nfsbxy  1895  nfsbxyt  1896  nfeud  1993  nfmod  1994  nfeqd  2273  nfeld  2274  nfabd  2277  nfned  2379  nfneld  2388  nfraldxy  2444  nfrexdxy  2445  nfraldya  2446  nfrexdya  2447  nfsbc1d  2898  nfsbcd  2901  nfbrd  3943
  Copyright terms: Public domain W3C validator