Theorem nfri 1543

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 1542	. 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 1371   F/wnf 1484

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

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

This theorem is referenced by:  alimd  1545  alrimi  1546  nfd  1547  nfrimi  1549  nfbidf  1563  19.3  1578  nfan1  1588  nfim1  1595  nfor  1598  nfimd  1609  exlimi  1618  exlimd  1621  eximd  1636  albid  1639  exbid  1640  nfex  1661  19.9  1668  nf2  1692  nf3  1693  spim  1762  cbv2  1773  cbvexv1  1776  cbval  1778  cbvex  1780  nfald  1784  nfexd  1785  sbf  1801  nfs1f  1804  sbied  1812  sbie  1815  nfs1  1833  equs5or  1854  sb4or  1857  sbid2  1874  cbvexd  1952  hbsb  1978  sbco2yz  1992  sbco2  1994  sbco3v  1998  sbcomxyyz  2001  nfsbd  2006  hbeu  2076  mo23  2097  mor  2098  eu2  2100  eu3  2102  mo2r  2108  mo3  2110  mo2dc  2111  moexexdc  2140  nfsab  2199  nfcrii  2343  bj-sbime  15909