Theorem nfri 1499

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

Syntax hints:   → wi 4  ∀wal 1329  Ⅎwnf 1436

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

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

This theorem is referenced by:  alimd  1501  alrimi  1502  nfd  1503  nfrimi  1505  nfbidf  1519  19.3  1533  nfan1  1543  nfim1  1550  nfor  1553  nfal  1555  nfimd  1564  exlimi  1573  exlimd  1576  eximd  1591  albid  1594  exbid  1595  nfex  1616  19.9  1623  nf2  1646  nf3  1647  spim  1716  cbv2  1725  cbval  1727  cbvex  1729  nfald  1733  nfexd  1734  sbf  1750  nfs1f  1753  sbied  1761  sbie  1764  nfs1  1781  equs5or  1802  sb4or  1805  sbid2  1822  cbvexd  1899  hbsb  1922  sbco2yz  1936  sbco2  1938  sbco3v  1942  sbcomxyyz  1945  nfsbd  1950  hbeu  2020  mo23  2040  mor  2041  eu2  2043  eu3  2045  mo2r  2051  mo3  2053  mo2dc  2054  moexexdc  2083  nfsab  2131  nfcrii  2274  bj-sbime  12980