Theorem nfri 1568

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

Syntax hints:   → wi 4  ∀wal 1396  Ⅎwnf 1509

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

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

This theorem is referenced by:  alimd  1570  alrimi  1571  nfd  1572  nfrimi  1574  nfbidf  1588  19.3  1603  nfan1  1613  nfim1  1620  nfor  1623  nfimd  1634  exlimi  1643  exlimd  1646  eximd  1661  albid  1664  exbid  1665  nfex  1686  19.9  1693  nf2  1716  nf3  1717  spim  1786  cbv2  1797  cbvexv1  1800  cbval  1802  cbvex  1804  nfald  1808  nfexd  1809  sbf  1825  nfs1f  1828  sbied  1836  sbie  1839  nfs1  1857  equs5or  1878  sb4or  1881  sbid2  1898  cbvexd  1976  hbsb  2002  sbco2yz  2016  sbco2  2018  sbco3v  2022  sbcomxyyz  2025  nfsbd  2030  hbeu  2100  mo23  2121  mor  2122  eu2  2124  eu3  2126  mo2r  2132  mo3  2134  mo2dc  2135  moexexdc  2164  nfsab  2223  nfcrii  2368  bj-sbime  16474