Theorem nfri 1455

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 1454	. 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 1285   F/wnf 1392

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

This theorem depends on definitions:  df-bi 115  df-nf 1393

This theorem is referenced by:  alimd  1457  alrimi  1458  nfd  1459  nfrimi  1461  nfbidf  1475  19.3  1489  nfan1  1499  nfim1  1506  nfor  1509  nfal  1511  nfimd  1520  exlimi  1528  exlimd  1531  eximd  1546  albid  1549  exbid  1550  nfex  1571  19.9  1578  nf2  1601  nf3  1602  spim  1670  cbv2  1679  cbval  1681  cbvex  1683  nfald  1687  nfexd  1688  sbf  1704  nfs1f  1707  sbied  1715  sbie  1718  nfs1  1734  equs5or  1755  sb4or  1758  sbid2  1775  cbvexd  1847  hbsb  1868  sbco2yz  1882  sbco2  1884  sbco3v  1888  sbcomxyyz  1891  nfsbd  1896  hbeu  1966  mo23  1986  mor  1987  eu2  1989  eu3  1991  mo2r  1997  mo3  1999  mo2dc  2000  moexexdc  2029  nfsab  2077  nfcrii  2218  bj-sbime  11119