Theorem nfri 1542

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 1541	. 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 1483

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

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

This theorem is referenced by:  alimd  1544  alrimi  1545  nfd  1546  nfrimi  1548  nfbidf  1562  19.3  1577  nfan1  1587  nfim1  1594  nfor  1597  nfimd  1608  exlimi  1617  exlimd  1620  eximd  1635  albid  1638  exbid  1639  nfex  1660  19.9  1667  nf2  1691  nf3  1692  spim  1761  cbv2  1772  cbvexv1  1775  cbval  1777  cbvex  1779  nfald  1783  nfexd  1784  sbf  1800  nfs1f  1803  sbied  1811  sbie  1814  nfs1  1832  equs5or  1853  sb4or  1856  sbid2  1873  cbvexd  1951  hbsb  1977  sbco2yz  1991  sbco2  1993  sbco3v  1997  sbcomxyyz  2000  nfsbd  2005  hbeu  2075  mo23  2095  mor  2096  eu2  2098  eu3  2100  mo2r  2106  mo3  2108  mo2dc  2109  moexexdc  2138  nfsab  2197  nfcrii  2341  bj-sbime  15709