Theorem nfri 1500

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 1499	. 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 1330   F/wnf 1437

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

This theorem depends on definitions:  df-bi 116  df-nf 1438

This theorem is referenced by:  alimd  1502  alrimi  1503  nfd  1504  nfrimi  1506  nfbidf  1520  19.3  1534  nfan1  1544  nfim1  1551  nfor  1554  nfal  1556  nfimd  1565  exlimi  1574  exlimd  1577  eximd  1592  albid  1595  exbid  1596  nfex  1617  19.9  1624  nf2  1647  nf3  1648  spim  1717  cbv2  1726  cbval  1728  cbvex  1730  nfald  1734  nfexd  1735  sbf  1751  nfs1f  1754  sbied  1762  sbie  1765  nfs1  1782  equs5or  1803  sb4or  1806  sbid2  1823  cbvexd  1900  hbsb  1923  sbco2yz  1937  sbco2  1939  sbco3v  1943  sbcomxyyz  1946  nfsbd  1951  hbeu  2021  mo23  2041  mor  2042  eu2  2044  eu3  2046  mo2r  2052  mo3  2054  mo2dc  2055  moexexdc  2084  nfsab  2132  nfcrii  2275  bj-sbime  13151