Theorem nfri 1512

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

Syntax hints:   → wi 4  ∀wal 1346  Ⅎwnf 1453

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

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

This theorem is referenced by:  alimd  1514  alrimi  1515  nfd  1516  nfrimi  1518  nfbidf  1532  19.3  1547  nfan1  1557  nfim1  1564  nfor  1567  nfimd  1578  exlimi  1587  exlimd  1590  eximd  1605  albid  1608  exbid  1609  nfex  1630  19.9  1637  nf2  1661  nf3  1662  spim  1731  cbv2  1742  cbvexv1  1745  cbval  1747  cbvex  1749  nfald  1753  nfexd  1754  sbf  1770  nfs1f  1773  sbied  1781  sbie  1784  nfs1  1802  equs5or  1823  sb4or  1826  sbid2  1843  cbvexd  1920  hbsb  1942  sbco2yz  1956  sbco2  1958  sbco3v  1962  sbcomxyyz  1965  nfsbd  1970  hbeu  2040  mo23  2060  mor  2061  eu2  2063  eu3  2065  mo2r  2071  mo3  2073  mo2dc  2074  moexexdc  2103  nfsab  2162  nfcrii  2305  bj-sbime  13808