Theorem nfri 1409

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 1408	. 2 |- ( F/xph -> (ph -> A.xph))
3	1, 2	ax-mp 7	1 |- (ph -> A.xph)

Syntax hints:   -> wi 4  A.wal 1240   F/wnf 1346

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

This theorem depends on definitions:  df-bi 110  df-nf 1347

This theorem is referenced by:  alimd  1411  alrimi  1412  nfd  1413  nfrimi  1415  nfbidf  1429  19.3  1443  nfan1  1453  nfim1  1460  nfor  1463  nfal  1465  nfimd  1474  exlimi  1482  exlimd  1485  eximd  1500  albid  1503  exbid  1504  nfex  1525  19.9  1532  nf2  1555  nf3  1556  spim  1623  cbv2  1632  cbval  1634  cbvex  1636  nfald  1640  nfexd  1641  sbf  1657  nfs1f  1660  sbied  1668  sbie  1671  nfs1  1687  equs5or  1708  sb4or  1711  sbid2  1727  cbvexd  1799  hbsb  1820  sbco2yz  1834  sbco2  1836  sbco3v  1840  sbcomxyyz  1843  nfsbd  1848  hbeu  1918  mo23  1938  mor  1939  eu2  1941  eu3  1943  mo2r  1949  mo3  1951  mo2dc  1952  moexexdc  1981  nfsab  2029  nfcrii  2168  bj-sbime  9248