Theorem nfri 1412

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 1411	. 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 1241   F/wnf 1349

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

This theorem depends on definitions:  df-bi 110  df-nf 1350

This theorem is referenced by:  alimd  1414  alrimi  1415  nfd  1416  nfrimi  1418  nfbidf  1432  19.3  1446  nfan1  1456  nfim1  1463  nfor  1466  nfal  1468  nfimd  1477  exlimi  1485  exlimd  1488  eximd  1503  albid  1506  exbid  1507  nfex  1528  19.9  1535  nf2  1558  nf3  1559  spim  1626  cbv2  1635  cbval  1637  cbvex  1639  nfald  1643  nfexd  1644  sbf  1660  nfs1f  1663  sbied  1671  sbie  1674  nfs1  1690  equs5or  1711  sb4or  1714  sbid2  1730  cbvexd  1802  hbsb  1823  sbco2yz  1837  sbco2  1839  sbco3v  1843  sbcomxyyz  1846  nfsbd  1851  hbeu  1921  mo23  1941  mor  1942  eu2  1944  eu3  1946  mo2r  1952  mo3  1954  mo2dc  1955  moexexdc  1984  nfsab  2032  nfcrii  2171  bj-sbime  9913