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

Theorem nfi 1473
Description: Deduce that  x is not free in  ph from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfi.1  |-  ( ph  ->  A. x ph )
Assertion
Ref Expression
nfi  |-  F/ x ph

Proof of Theorem nfi
StepHypRef Expression
1 df-nf 1472 . 2  |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
2 nfi.1 . 2  |-  ( ph  ->  A. x ph )
31, 2mpgbir 1464 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1362   F/wnf 1471
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-gen 1460
This theorem depends on definitions:  df-bi 117  df-nf 1472
This theorem is referenced by:  nfth  1475  nfnth  1476  nfe1  1507  nfdh  1535  nfv  1539  nfa1  1552  nfan1  1575  nfim1  1582  nfor  1585  nfex  1648  nfae  1730  cbv3h  1754  nfs1  1820  nfs1v  1951  hbsb  1961  sbco2h  1976  hbsbd  1994  dvelimALT  2022  dvelimfv  2023  hbeu  2059  hbeud  2060  eu3h  2083  mo3h  2091  nfsab1  2179  nfsab  2181  nfcii  2323  nfcri  2326
  Copyright terms: Public domain W3C validator