Theorem nfri 1568

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 1567	. 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 1396   F/wnf 1509

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

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

This theorem is referenced by:  alimd  1570  alrimi  1571  nfd  1572  nfrimi  1574  nfbidf  1588  19.3  1603  nfan1  1613  nfim1  1620  nfor  1623  nfimd  1634  exlimi  1643  exlimd  1646  eximd  1661  albid  1664  exbid  1665  nfex  1686  19.9  1693  nf2  1716  nf3  1717  spim  1787  cbv2  1798  cbvexv1  1801  cbval  1803  cbvex  1805  nfald  1809  nfexd  1810  sbf  1826  nfs1f  1829  sbied  1837  sbie  1840  nfs1  1858  equs5or  1879  sb4or  1882  sbid2  1899  cbvexd  1977  hbsb  2003  sbco2yz  2017  sbco2  2019  sbco3v  2023  sbcomxyyz  2026  nfsbd  2031  hbeu  2101  mo23  2122  mor  2123  eu2  2125  eu3  2127  mo2r  2133  mo3  2135  mo2dc  2136  moexexdc  2165  nfsab  2224  nfcrii  2377  bj-sbime  16545