Theorem nfri 1565

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

Syntax hints:   → wi 4  ∀wal 1393  Ⅎwnf 1506

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

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

This theorem is referenced by:  alimd  1567  alrimi  1568  nfd  1569  nfrimi  1571  nfbidf  1585  19.3  1600  nfan1  1610  nfim1  1617  nfor  1620  nfimd  1631  exlimi  1640  exlimd  1643  eximd  1658  albid  1661  exbid  1662  nfex  1683  19.9  1690  nf2  1714  nf3  1715  spim  1784  cbv2  1795  cbvexv1  1798  cbval  1800  cbvex  1802  nfald  1806  nfexd  1807  sbf  1823  nfs1f  1826  sbied  1834  sbie  1837  nfs1  1855  equs5or  1876  sb4or  1879  sbid2  1896  cbvexd  1974  hbsb  2000  sbco2yz  2014  sbco2  2016  sbco3v  2020  sbcomxyyz  2023  nfsbd  2028  hbeu  2098  mo23  2119  mor  2120  eu2  2122  eu3  2124  mo2r  2130  mo3  2132  mo2dc  2133  moexexdc  2162  nfsab  2221  nfcrii  2365  bj-sbime  16095