Theorem nfri 1519

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

Syntax hints:   → wi 4  ∀wal 1351  Ⅎwnf 1460

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

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

This theorem is referenced by:  alimd  1521  alrimi  1522  nfd  1523  nfrimi  1525  nfbidf  1539  19.3  1554  nfan1  1564  nfim1  1571  nfor  1574  nfimd  1585  exlimi  1594  exlimd  1597  eximd  1612  albid  1615  exbid  1616  nfex  1637  19.9  1644  nf2  1668  nf3  1669  spim  1738  cbv2  1749  cbvexv1  1752  cbval  1754  cbvex  1756  nfald  1760  nfexd  1761  sbf  1777  nfs1f  1780  sbied  1788  sbie  1791  nfs1  1809  equs5or  1830  sb4or  1833  sbid2  1850  cbvexd  1927  hbsb  1949  sbco2yz  1963  sbco2  1965  sbco3v  1969  sbcomxyyz  1972  nfsbd  1977  hbeu  2047  mo23  2067  mor  2068  eu2  2070  eu3  2072  mo2r  2078  mo3  2080  mo2dc  2081  moexexdc  2110  nfsab  2169  nfcrii  2312  bj-sbime  14564