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

Theorem nfri 1389
Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfri.1 xφ
Assertion
Ref Expression
nfri (φxφ)

Proof of Theorem nfri
StepHypRef Expression
1 nfri.1 . 2 xφ
2 nfr 1388 . 2 (Ⅎxφ → (φxφ))
31, 2ax-mp 7 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-4 1377
This theorem depends on definitions:  df-bi 110  df-nf 1326
This theorem is referenced by:  alimd  1391  alrimi  1392  nfd  1393  nfrimi  1395  nfbidf  1410  19.3  1424  nfan1  1434  nfim1  1441  nfor  1444  nfal  1446  nfimd  1455  exlimi  1463  exlimd  1466  eximd  1481  albid  1484  exbid  1485  nfex  1506  19.9  1513  nf2  1536  nf3  1537  spim  1604  cbv2  1613  cbval  1615  cbvex  1617  nfald  1621  nfexd  1622  sbf  1638  nfs1f  1641  sbied  1649  sbie  1652  nfs1  1668  equs5or  1689  sb4or  1692  sbid2  1708  cbvexd  1780  hbsb  1801  sbco2yz  1815  sbco2  1817  sbco3v  1821  sbcomxyyz  1824  nfsbd  1829  hbeu  1899  mo23  1919  mor  1920  eu2  1922  eu3  1924  mo2r  1930  mo3  1932  mo2dc  1933  moexexdc  1962  nfsab  2010  nfcrii  2149  bj-sbime  7159
  Copyright terms: Public domain W3C validator