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

Theorem nfri 1409
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 1408 . 2 (Ⅎxφ → (φxφ))
31, 2ax-mp 7 1 (φxφ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1240  wnf 1346
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-4 1397
This theorem depends on definitions:  df-bi 110  df-nf 1347
This theorem is referenced by:  alimd  1411  alrimi  1412  nfd  1413  nfrimi  1415  nfbidf  1429  19.3  1443  nfan1  1453  nfim1  1460  nfor  1463  nfal  1465  nfimd  1474  exlimi  1482  exlimd  1485  eximd  1500  albid  1503  exbid  1504  nfex  1525  19.9  1532  nf2  1555  nf3  1556  spim  1623  cbv2  1632  cbval  1634  cbvex  1636  nfald  1640  nfexd  1641  sbf  1657  nfs1f  1660  sbied  1668  sbie  1671  nfs1  1687  equs5or  1708  sb4or  1711  sbid2  1727  cbvexd  1799  hbsb  1820  sbco2yz  1834  sbco2  1836  sbco3v  1840  sbcomxyyz  1843  nfsbd  1848  hbeu  1918  mo23  1938  mor  1939  eu2  1941  eu3  1943  mo2r  1949  mo3  1951  mo2dc  1952  moexexdc  1981  nfsab  2029  nfcrii  2168  bj-sbime  9228
  Copyright terms: Public domain W3C validator