Theorem nfri 1533

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 1532	. 2 |- ( F/ x ph -> ( ph -> A. x ph ) )
3	1, 2	ax-mp 5	1 |- ( ph -> A. x ph )

Syntax hints:   -> wi 4   A.wal 1362   F/wnf 1474

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

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

This theorem is referenced by:  alimd  1535  alrimi  1536  nfd  1537  nfrimi  1539  nfbidf  1553  19.3  1568  nfan1  1578  nfim1  1585  nfor  1588  nfimd  1599  exlimi  1608  exlimd  1611  eximd  1626  albid  1629  exbid  1630  nfex  1651  19.9  1658  nf2  1682  nf3  1683  spim  1752  cbv2  1763  cbvexv1  1766  cbval  1768  cbvex  1770  nfald  1774  nfexd  1775  sbf  1791  nfs1f  1794  sbied  1802  sbie  1805  nfs1  1823  equs5or  1844  sb4or  1847  sbid2  1864  cbvexd  1942  hbsb  1968  sbco2yz  1982  sbco2  1984  sbco3v  1988  sbcomxyyz  1991  nfsbd  1996  hbeu  2066  mo23  2086  mor  2087  eu2  2089  eu3  2091  mo2r  2097  mo3  2099  mo2dc  2100  moexexdc  2129  nfsab  2188  nfcrii  2332  bj-sbime  15419