Theorem nfri 1517

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 1516	. 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 1351   F/wnf 1458

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

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

This theorem is referenced by:  alimd  1519  alrimi  1520  nfd  1521  nfrimi  1523  nfbidf  1537  19.3  1552  nfan1  1562  nfim1  1569  nfor  1572  nfimd  1583  exlimi  1592  exlimd  1595  eximd  1610  albid  1613  exbid  1614  nfex  1635  19.9  1642  nf2  1666  nf3  1667  spim  1736  cbv2  1747  cbvexv1  1750  cbval  1752  cbvex  1754  nfald  1758  nfexd  1759  sbf  1775  nfs1f  1778  sbied  1786  sbie  1789  nfs1  1807  equs5or  1828  sb4or  1831  sbid2  1848  cbvexd  1925  hbsb  1947  sbco2yz  1961  sbco2  1963  sbco3v  1967  sbcomxyyz  1970  nfsbd  1975  hbeu  2045  mo23  2065  mor  2066  eu2  2068  eu3  2070  mo2r  2076  mo3  2078  mo2dc  2079  moexexdc  2108  nfsab  2167  nfcrii  2310  bj-sbime  14083