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

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

Proof of Theorem nfi
StepHypRef Expression
1 df-nf 1347 . 2  F/
2 nfi.1 . 2
31, 2mpgbir 1339 1  F/
Colors of variables: wff set class
Syntax hints:   wi 4  wal 1240   F/wnf 1346
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 1335
This theorem depends on definitions:  df-bi 110  df-nf 1347
This theorem is referenced by:  nfth  1350  nfnth  1351  nfe1  1382  nfdh  1414  nfv  1418  nfa1  1431  nfan1  1453  nfim1  1460  nfor  1463  nfal  1465  nfex  1525  nfae  1604  cbv3h  1628  nfs1  1687  nfs1v  1812  hbsb  1820  sbco2h  1835  hbsbd  1855  dvelimALT  1883  dvelimfv  1884  hbeu  1918  hbeud  1919  eu3h  1942  mo3h  1950  nfsab1  2027  nfsab  2029  nfcii  2166  nfcri  2169
  Copyright terms: Public domain W3C validator