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

Theorem nfri 1457
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 1456 . 2 (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
31, 2ax-mp 7 1 (𝜑 → ∀𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1287  wnf 1394
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-4 1445
This theorem depends on definitions:  df-bi 115  df-nf 1395
This theorem is referenced by:  alimd  1459  alrimi  1460  nfd  1461  nfrimi  1463  nfbidf  1477  19.3  1491  nfan1  1501  nfim1  1508  nfor  1511  nfal  1513  nfimd  1522  exlimi  1530  exlimd  1533  eximd  1548  albid  1551  exbid  1552  nfex  1573  19.9  1580  nf2  1603  nf3  1604  spim  1673  cbv2  1682  cbval  1684  cbvex  1686  nfald  1690  nfexd  1691  sbf  1707  nfs1f  1710  sbied  1718  sbie  1721  nfs1  1737  equs5or  1758  sb4or  1761  sbid2  1778  cbvexd  1850  hbsb  1871  sbco2yz  1885  sbco2  1887  sbco3v  1891  sbcomxyyz  1894  nfsbd  1899  hbeu  1969  mo23  1989  mor  1990  eu2  1992  eu3  1994  mo2r  2000  mo3  2002  mo2dc  2003  moexexdc  2032  nfsab  2080  nfcrii  2221  bj-sbime  11331
  Copyright terms: Public domain W3C validator