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