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  1961  sbco2yz  1975  sbco2  1977  sbco3v  1981  sbcomxyyz  1984  nfsbd  1989  hbeu  2059  mo23  2079  mor  2080  eu2  2082  eu3  2084  mo2r  2090  mo3  2092  mo2dc  2093  moexexdc  2122  nfsab  2181  nfcrii  2325  bj-sbime  15003