Theorem nfri 1762

Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfri.1	|- F/xph

Assertion

Ref	Expression
nfri	|- (ph -> A.xph)

Proof of Theorem nfri

Step	Hyp	Ref	Expression
1		nfri.1	. 2 |- F/xph
2		nfr 1761	. 2 |- ( F/xph -> (ph -> A.xph))
3	1, 2	ax-mp 5	1 |- (ph -> A.xph)

Syntax hints:   -> wi 4  A.wal 1540   F/wnf 1544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545

This theorem is referenced by:  alimd  1764  alrimi  1765  eximd  1770  nexd  1771  albid  1772  exbid  1773  19.9  1783  19.3  1785  stdpc5OLD  1799  nfim1  1811  hban  1828  hb3an  1830  nfal  1842  nfex  1843  equsal  1960  equs45f  1989  cbvald  2008  sb6f  2039  nfs1  2044  hbsb  2110  nfsab  2345  nfcrii  2482