Theorem nfri 1507

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 1506	. 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 1341   F/wnf 1448

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

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

This theorem is referenced by:  alimd  1509  alrimi  1510  nfd  1511  nfrimi  1513  nfbidf  1527  19.3  1542  nfan1  1552  nfim1  1559  nfor  1562  nfimd  1573  exlimi  1582  exlimd  1585  eximd  1600  albid  1603  exbid  1604  nfex  1625  19.9  1632  nf2  1656  nf3  1657  spim  1726  cbv2  1737  cbvexv1  1740  cbval  1742  cbvex  1744  nfald  1748  nfexd  1749  sbf  1765  nfs1f  1768  sbied  1776  sbie  1779  nfs1  1797  equs5or  1818  sb4or  1821  sbid2  1838  cbvexd  1915  hbsb  1937  sbco2yz  1951  sbco2  1953  sbco3v  1957  sbcomxyyz  1960  nfsbd  1965  hbeu  2035  mo23  2055  mor  2056  eu2  2058  eu3  2060  mo2r  2066  mo3  2068  mo2dc  2069  moexexdc  2098  nfsab  2157  nfcrii  2301  bj-sbime  13654