Theorem nfri 1452

Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfri.1	|- F/ x ph

Assertion

Ref	Expression
nfri	|- ( ph -> A. x ph )

Proof of Theorem nfri

Step	Hyp	Ref	Expression
1		nfri.1	. 2 |- F/ x ph
2		nfr 1451	. 2 |- ( F/ x ph -> ( ph -> A. x ph ) )
3	1, 2	ax-mp 7	1 |- ( ph -> A. x ph )

Syntax hints:   -> wi 4   A.wal 1282   F/wnf 1389

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

This theorem depends on definitions:  df-bi 115  df-nf 1390

This theorem is referenced by:  alimd  1454  alrimi  1455  nfd  1456  nfrimi  1458  nfbidf  1472  19.3  1486  nfan1  1496  nfim1  1503  nfor  1506  nfal  1508  nfimd  1517  exlimi  1525  exlimd  1528  eximd  1543  albid  1546  exbid  1547  nfex  1568  19.9  1575  nf2  1598  nf3  1599  spim  1666  cbv2  1675  cbval  1677  cbvex  1679  nfald  1683  nfexd  1684  sbf  1700  nfs1f  1703  sbied  1711  sbie  1714  nfs1  1730  equs5or  1751  sb4or  1754  sbid2  1771  cbvexd  1843  hbsb  1864  sbco2yz  1878  sbco2  1880  sbco3v  1884  sbcomxyyz  1887  nfsbd  1892  hbeu  1962  mo23  1982  mor  1983  eu2  1985  eu3  1987  mo2r  1993  mo3  1995  mo2dc  1996  moexexdc  2025  nfsab  2073  nfcrii  2212  bj-sbime  10584