Theorem nfri 1506

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 1505	. 2 ⊢ (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝜑 → ∀𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1340  Ⅎwnf 1447

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

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

This theorem is referenced by:  alimd  1508  alrimi  1509  nfd  1510  nfrimi  1512  nfbidf  1526  19.3  1541  nfan1  1551  nfim1  1558  nfor  1561  nfimd  1572  exlimi  1581  exlimd  1584  eximd  1599  albid  1602  exbid  1603  nfex  1624  19.9  1631  nf2  1655  nf3  1656  spim  1725  cbv2  1736  cbvexv1  1739  cbval  1741  cbvex  1743  nfald  1747  nfexd  1748  sbf  1764  nfs1f  1767  sbied  1775  sbie  1778  nfs1  1796  equs5or  1817  sb4or  1820  sbid2  1837  cbvexd  1914  hbsb  1936  sbco2yz  1950  sbco2  1952  sbco3v  1956  sbcomxyyz  1959  nfsbd  1964  hbeu  2034  mo23  2054  mor  2055  eu2  2057  eu3  2059  mo2r  2065  mo3  2067  mo2dc  2068  moexexdc  2097  nfsab  2156  nfcrii  2299  bj-sbime  13489