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

Theorem nfxfrd 1405
 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 1403 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3sylibr 132 1 (𝜒 → Ⅎ𝑥𝜑)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 103  Ⅎwnf 1390 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379 This theorem depends on definitions:  df-bi 115  df-nf 1391 This theorem is referenced by:  nf3and  1502  nfbid  1521  nfsbxy  1860  nfsbxyt  1861  nfeud  1958  nfmod  1959  nfeqd  2234  nfeld  2235  nfabd  2238  nfned  2339  nfneld  2348  nfraldxy  2399  nfrexdxy  2400  nfraldya  2401  nfrexdya  2402  nfsbc1d  2832  nfsbcd  2835  nfbrd  3830
 Copyright terms: Public domain W3C validator