Theorem nfri 1482

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

Step	Hyp	Ref	Expression
1		nfri.1	. 2 ⊢ Ⅎ𝑥𝜑
2		nfr 1481	. 2 ⊢ (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
3	1, 2	ax-mp 7	1 ⊢ (𝜑 → ∀𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1312  Ⅎwnf 1419

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-4 1470

This theorem depends on definitions:  df-bi 116  df-nf 1420

This theorem is referenced by:  alimd  1484  alrimi  1485  nfd  1486  nfrimi  1488  nfbidf  1502  19.3  1516  nfan1  1526  nfim1  1533  nfor  1536  nfal  1538  nfimd  1547  exlimi  1556  exlimd  1559  eximd  1574  albid  1577  exbid  1578  nfex  1599  19.9  1606  nf2  1629  nf3  1630  spim  1699  cbv2  1708  cbval  1710  cbvex  1712  nfald  1716  nfexd  1717  sbf  1733  nfs1f  1736  sbied  1744  sbie  1747  nfs1  1763  equs5or  1784  sb4or  1787  sbid2  1804  cbvexd  1877  hbsb  1898  sbco2yz  1912  sbco2  1914  sbco3v  1918  sbcomxyyz  1921  nfsbd  1926  hbeu  1996  mo23  2016  mor  2017  eu2  2019  eu3  2021  mo2r  2027  mo3  2029  mo2dc  2030  moexexdc  2059  nfsab  2107  nfcrii  2248  bj-sbime  12673