Theorem nfri 1467

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 1466	. 2 |- ( F/ x ph -> ( ph -> A. x ph ) )
3	1, 2	ax-mp 7	1 |- ( ph -> A. x ph )

Syntax hints:   -> wi 4   A.wal 1297   F/wnf 1404

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

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

This theorem is referenced by:  alimd  1469  alrimi  1470  nfd  1471  nfrimi  1473  nfbidf  1487  19.3  1501  nfan1  1511  nfim1  1518  nfor  1521  nfal  1523  nfimd  1532  exlimi  1541  exlimd  1544  eximd  1559  albid  1562  exbid  1563  nfex  1584  19.9  1591  nf2  1614  nf3  1615  spim  1684  cbv2  1693  cbval  1695  cbvex  1697  nfald  1701  nfexd  1702  sbf  1718  nfs1f  1721  sbied  1729  sbie  1732  nfs1  1748  equs5or  1769  sb4or  1772  sbid2  1789  cbvexd  1862  hbsb  1883  sbco2yz  1897  sbco2  1899  sbco3v  1903  sbcomxyyz  1906  nfsbd  1911  hbeu  1981  mo23  2001  mor  2002  eu2  2004  eu3  2006  mo2r  2012  mo3  2014  mo2dc  2015  moexexdc  2044  nfsab  2092  nfcrii  2233  bj-sbime  12562