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

Theorem nfri 1484
Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfri.1 𝑥𝜑
Assertion
Ref Expression
nfri (𝜑 → ∀𝑥𝜑)

Proof of Theorem nfri
StepHypRef Expression
1 nfri.1 . 2 𝑥𝜑
2 nfr 1483 . 2 (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
31, 2ax-mp 5 1 (𝜑 → ∀𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1314  wnf 1421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-4 1472
This theorem depends on definitions:  df-bi 116  df-nf 1422
This theorem is referenced by:  alimd  1486  alrimi  1487  nfd  1488  nfrimi  1490  nfbidf  1504  19.3  1518  nfan1  1528  nfim1  1535  nfor  1538  nfal  1540  nfimd  1549  exlimi  1558  exlimd  1561  eximd  1576  albid  1579  exbid  1580  nfex  1601  19.9  1608  nf2  1631  nf3  1632  spim  1701  cbv2  1710  cbval  1712  cbvex  1714  nfald  1718  nfexd  1719  sbf  1735  nfs1f  1738  sbied  1746  sbie  1749  nfs1  1765  equs5or  1786  sb4or  1789  sbid2  1806  cbvexd  1879  hbsb  1900  sbco2yz  1914  sbco2  1916  sbco3v  1920  sbcomxyyz  1923  nfsbd  1928  hbeu  1998  mo23  2018  mor  2019  eu2  2021  eu3  2023  mo2r  2029  mo3  2031  mo2dc  2032  moexexdc  2061  nfsab  2109  nfcrii  2251  bj-sbime  12907
  Copyright terms: Public domain W3C validator