Theorem nfri 1572

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

Syntax hints:   → wi 4  ∀wal 1400  Ⅎwnf 1513

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

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

This theorem is referenced by:  alimd  1574  alrimi  1575  nfd  1576  nfrimi  1578  nfbidf  1592  19.3  1607  nfan1  1617  nfim1  1624  nfor  1627  nfimd  1638  exlimi  1647  exlimd  1650  eximd  1665  albid  1668  exbid  1669  nfex  1690  19.9  1697  nf2  1720  nf3  1721  spim  1791  cbv2  1802  cbvexv1  1805  cbval  1807  cbvex  1809  nfald  1813  nfexd  1814  sbf  1830  nfs1f  1833  sbied  1841  sbie  1844  nfs1  1862  equs5or  1883  sb4or  1886  sbid2  1903  cbvexd  1983  hbsb  2009  sbco2yz  2023  sbco2  2025  sbco3v  2029  sbcomxyyz  2032  nfsbd  2037  hbeu  2107  mo23  2128  mor  2129  eu2  2131  eu3  2133  mo2r  2139  mo3  2141  mo2dc  2142  moexexdc  2171  nfsab  2230  nfcrii  2385  bj-sbime  16715