Theorem nfri 1530

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 1529	. 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 1471

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

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

This theorem is referenced by:  alimd  1532  alrimi  1533  nfd  1534  nfrimi  1536  nfbidf  1550  19.3  1565  nfan1  1575  nfim1  1582  nfor  1585  nfimd  1596  exlimi  1605  exlimd  1608  eximd  1623  albid  1626  exbid  1627  nfex  1648  19.9  1655  nf2  1679  nf3  1680  spim  1749  cbv2  1760  cbvexv1  1763  cbval  1765  cbvex  1767  nfald  1771  nfexd  1772  sbf  1788  nfs1f  1791  sbied  1799  sbie  1802  nfs1  1820  equs5or  1841  sb4or  1844  sbid2  1861  cbvexd  1939  hbsb  1965  sbco2yz  1979  sbco2  1981  sbco3v  1985  sbcomxyyz  1988  nfsbd  1993  hbeu  2063  mo23  2083  mor  2084  eu2  2086  eu3  2088  mo2r  2094  mo3  2096  mo2dc  2097  moexexdc  2126  nfsab  2185  nfcrii  2329  bj-sbime  15265