Theorem nfri 1567

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

Syntax hints:   → wi 4  ∀wal 1395  Ⅎwnf 1508

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

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

This theorem is referenced by:  alimd  1569  alrimi  1570  nfd  1571  nfrimi  1573  nfbidf  1587  19.3  1602  nfan1  1612  nfim1  1619  nfor  1622  nfimd  1633  exlimi  1642  exlimd  1645  eximd  1660  albid  1663  exbid  1664  nfex  1685  19.9  1692  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  2367  bj-sbime  16369