Theorem nfri 1541

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

Syntax hints:   → wi 4  ∀wal 1370  Ⅎwnf 1482

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

This theorem depends on definitions:  df-bi 117  df-nf 1483

This theorem is referenced by:  alimd  1543  alrimi  1544  nfd  1545  nfrimi  1547  nfbidf  1561  19.3  1576  nfan1  1586  nfim1  1593  nfor  1596  nfimd  1607  exlimi  1616  exlimd  1619  eximd  1634  albid  1637  exbid  1638  nfex  1659  19.9  1666  nf2  1690  nf3  1691  spim  1760  cbv2  1771  cbvexv1  1774  cbval  1776  cbvex  1778  nfald  1782  nfexd  1783  sbf  1799  nfs1f  1802  sbied  1810  sbie  1813  nfs1  1831  equs5or  1852  sb4or  1855  sbid2  1872  cbvexd  1950  hbsb  1976  sbco2yz  1990  sbco2  1992  sbco3v  1996  sbcomxyyz  1999  nfsbd  2004  hbeu  2074  mo23  2094  mor  2095  eu2  2097  eu3  2099  mo2r  2105  mo3  2107  mo2dc  2108  moexexdc  2137  nfsab  2196  nfcrii  2340  bj-sbime  15573