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  1979  hbsb  2005  sbco2yz  2019  sbco2  2021  sbco3v  2025  sbcomxyyz  2028  nfsbd  2033  hbeu  2103  mo23  2124  mor  2125  eu2  2127  eu3  2129  mo2r  2135  mo3  2137  mo2dc  2138  moexexdc  2167  nfsab  2226  nfcrii  2379  bj-sbime  16671