Theorem nfimd 1977

Description: If in a context x is not free in ps and ch, it is not free in ( ps -> ch ). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)

Hypotheses

Ref	Expression
nfimd.1	|- ( ph -> F/ x ps )
nfimd.2	|- ( ph -> F/ x ch )

Assertion

Ref	Expression
nfimd	|- ( ph -> F/ x ( ps -> ch ) )

Proof of Theorem nfimd

Step	Hyp	Ref	Expression
1		nfimd.1	. 2 |- ( ph -> F/ x ps )
2		nfimd.2	. 2 |- ( ph -> F/ x ch )
3		nfnf1 1958	. . . 4 |- F/ x F/ x ps
4		nfnf1 1958	. . . 4 |- F/ x F/ x ch
5		nfr 1928	. . . . . 6 |- ( F/ x ch -> ( ch -> A. x ch ) )
6	5	imim2d 54	. . . . 5 |- ( F/ x ch -> ( ( ps -> ch ) -> ( ps -> A. x ch ) ) )
7		19.21t 1963	. . . . . 6 |- ( F/ x ps -> ( A. x ( ps -> ch ) <-> ( ps -> A. x ch ) ) )
8	7	biimprd 226	. . . . 5 |- ( F/ x ps -> ( ( ps -> A. x ch ) -> A. x ( ps -> ch ) ) )
9	6, 8	syl9r 74	. . . 4 |- ( F/ x ps -> ( F/ x ch -> ( ( ps -> ch ) -> A. x ( ps -> ch ) ) ) )
10	3, 4, 9	alrimd 1936	. . 3 |- ( F/ x ps -> ( F/ x ch -> A. x ( ( ps -> ch ) -> A. x ( ps -> ch ) ) ) )
11		df-nf 1662	. . 3 |- ( F/ x ( ps -> ch ) <-> A. x ( ( ps -> ch ) -> A. x ( ps -> ch ) ) )
12	10, 11	syl6ibr 230	. 2 |- ( F/ x ps -> ( F/ x ch -> F/ x ( ps -> ch ) ) )
13	1, 2, 12	sylc 62	1 |- ( ph -> F/ x ( ps -> ch ) )

Syntax hints:   -> wi 4   A.wal 1435   F/wnf 1661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-12 1909

This theorem depends on definitions:  df-bi 188  df-ex 1658  df-nf 1662

This theorem is referenced by:  hbimd  1981  nfand  1985  nfbid  1993  dvelimhw  2037  dvelimf  2142  nfmod2  2289  nfrald  2750  nfifd  3882  nfixp  7496  axrepndlem1  8968  axrepndlem2  8969  axunndlem1  8971  axunnd  8972  axpowndlem2  8974  axpowndlem3  8975  axpowndlem4  8976  axregndlem2  8979  axregnd  8980  axinfndlem1  8981  axinfnd  8982  axacndlem4  8986  axacndlem5  8987  axacnd  8988  wl-mo2df  31806  wl-mo2t  31811  riotasv2d  32441