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

Theorem nfxfrd 1344
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 (χ → Ⅎxψ)
Assertion
Ref Expression
nfxfrd (χ → Ⅎxφ)

Proof of Theorem nfxfrd
StepHypRef Expression
1 nfxfrd.2 . 2 (χ → Ⅎxψ)
2 nfbii.1 . . 3 (φψ)
32nfbii 1342 . 2 (Ⅎxφ ↔ Ⅎxψ)
41, 3sylibr 137 1 (χ → Ⅎxφ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wnf 1329
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318
This theorem depends on definitions:  df-bi 110  df-nf 1330
This theorem is referenced by:  nf3and  1443  nfbid  1462  nfsbxy  1800  nfsbxyt  1801  nfeud  1898  nfmod  1899  nfeqd  2174  nfeld  2175  nfabd  2178  nfned  2276  nfneld  2283  nfraldxy  2334  nfrexdxy  2335  nfraldya  2336  nfrexdya  2337  nfsbc1d  2757  nfsbcd  2760  nfbrd  3781
  Copyright terms: Public domain W3C validator