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

Theorem nfxfrd 1497
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  |-  ( ph  <->  ps )
nfxfrd.2  |-  ( ch 
->  F/ x ps )
Assertion
Ref Expression
nfxfrd  |-  ( ch 
->  F/ x ph )

Proof of Theorem nfxfrd
StepHypRef Expression
1 nfxfrd.2 . 2  |-  ( ch 
->  F/ x ps )
2 nfbii.1 . . 3  |-  ( ph  <->  ps )
32nfbii 1495 . 2  |-  ( F/ x ph  <->  F/ x ps )
41, 3sylibr 134 1  |-  ( ch 
->  F/ x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105   F/wnf 1482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471
This theorem depends on definitions:  df-bi 117  df-nf 1483
This theorem is referenced by:  nf3and  1591  nfbid  1610  nfsbxy  1969  nfsbxyt  1970  nfeud  2069  nfmod  2070  nfeqd  2362  nfeld  2363  nfabdw  2366  nfabd  2367  nfned  2469  nfneld  2478  nfraldw  2537  nfraldxy  2538  nfrexdxy  2539  nfraldya  2540  nfrexdya  2541  nfsbc1d  3014  nfsbcd  3017  nfsbcdw  3126  nfbrd  4088
  Copyright terms: Public domain W3C validator