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

Theorem nfi 1327
Description: Deduce that x is not free in φ from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfi.1 (φxφ)
Assertion
Ref Expression
nfi xφ

Proof of Theorem nfi
StepHypRef Expression
1 df-nf 1326 . 2 (Ⅎxφx(φxφ))
2 nfi.1 . 2 (φxφ)
31, 2mpgbir 1318 1 xφ
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1224  wnf 1325
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-gen 1314
This theorem depends on definitions:  df-bi 110  df-nf 1326
This theorem is referenced by:  nfth  1329  nfnth  1330  nfe1  1362  nfdh  1394  nfv  1398  nfa1  1412  nfan1  1434  nfim1  1441  nfor  1444  nfal  1446  nfex  1506  nfae  1585  cbv3h  1609  nfs1  1668  nfs1v  1793  hbsb  1801  sbco2h  1816  hbsbd  1836  dvelimALT  1864  dvelimfv  1865  hbeu  1899  hbeud  1900  eu3h  1923  mo3h  1931  nfsab1  2008  nfsab  2010  nfcii  2147  nfcri  2150
  Copyright terms: Public domain W3C validator