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

Theorem nfxfrd 1407
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 1405 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3sylibr 132 1 (𝜒 → Ⅎ𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wnf 1392
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 1379  ax-gen 1381
This theorem depends on definitions:  df-bi 115  df-nf 1393
This theorem is referenced by:  nf3and  1504  nfbid  1523  nfsbxy  1863  nfsbxyt  1864  nfeud  1961  nfmod  1962  nfeqd  2239  nfeld  2240  nfabd  2243  nfned  2345  nfneld  2354  nfraldxy  2406  nfrexdxy  2407  nfraldya  2408  nfrexdya  2409  nfsbc1d  2845  nfsbcd  2848  nfbrd  3862
  Copyright terms: Public domain W3C validator