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

Theorem nfxfrd 1498
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 1496 . 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 1483
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 1470  ax-gen 1472
This theorem depends on definitions:  df-bi 117  df-nf 1484
This theorem is referenced by:  nf3and  1592  nfbid  1611  nfsbxy  1970  nfsbxyt  1971  nfeud  2070  nfmod  2071  nfeqd  2363  nfeld  2364  nfabdw  2367  nfabd  2368  nfned  2470  nfneld  2479  nfraldw  2538  nfraldxy  2539  nfrexdxy  2540  nfraldya  2541  nfrexdya  2542  nfsbc1d  3015  nfsbcd  3018  nfsbcdw  3127  nfbrd  4089
  Copyright terms: Public domain W3C validator