Theorem nfri 1543

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

Syntax hints:   → wi 4  ∀wal 1371  Ⅎwnf 1484

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

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

This theorem is referenced by:  alimd  1545  alrimi  1546  nfd  1547  nfrimi  1549  nfbidf  1563  19.3  1578  nfan1  1588  nfim1  1595  nfor  1598  nfimd  1609  exlimi  1618  exlimd  1621  eximd  1636  albid  1639  exbid  1640  nfex  1661  19.9  1668  nf2  1692  nf3  1693  spim  1762  cbv2  1773  cbvexv1  1776  cbval  1778  cbvex  1780  nfald  1784  nfexd  1785  sbf  1801  nfs1f  1804  sbied  1812  sbie  1815  nfs1  1833  equs5or  1854  sb4or  1857  sbid2  1874  cbvexd  1952  hbsb  1978  sbco2yz  1992  sbco2  1994  sbco3v  1998  sbcomxyyz  2001  nfsbd  2006  hbeu  2076  mo23  2096  mor  2097  eu2  2099  eu3  2101  mo2r  2107  mo3  2109  mo2dc  2110  moexexdc  2139  nfsab  2198  nfcrii  2342  bj-sbime  15848