Theorem nfimd 1859

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 1842	. . . 4 |- F/ x F/ x ps
4		nfnf1 1842	. . . 4 |- F/ x F/ x ch
5		nfr 1816	. . . . . 6 |- ( F/ x ch -> ( ch -> A. x ch ) )
6	5	imim2d 52	. . . . 5 |- ( F/ x ch -> ( ( ps -> ch ) -> ( ps -> A. x ch ) ) )
7		19.21t 1847	. . . . . 6 |- ( F/ x ps -> ( A. x ( ps -> ch ) <-> ( ps -> A. x ch ) ) )
8	7	biimprd 223	. . . . 5 |- ( F/ x ps -> ( ( ps -> A. x ch ) -> A. x ( ps -> ch ) ) )
9	6, 8	syl9r 72	. . . 4 |- ( F/ x ps -> ( F/ x ch -> ( ( ps -> ch ) -> A. x ( ps -> ch ) ) ) )
10	3, 4, 9	alrimd 1824	. . 3 |- ( F/ x ps -> ( F/ x ch -> A. x ( ( ps -> ch ) -> A. x ( ps -> ch ) ) ) )
11		df-nf 1595	. . 3 |- ( F/ x ( ps -> ch ) <-> A. x ( ( ps -> ch ) -> A. x ( ps -> ch ) ) )
12	10, 11	syl6ibr 227	. 2 |- ( F/ x ps -> ( F/ x ch -> F/ x ( ps -> ch ) ) )
13	1, 2, 12	sylc 60	1 |- ( ph -> F/ x ( ps -> ch ) )

Syntax hints:   -> wi 4   A.wal 1372   F/wnf 1594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-12 1798

This theorem depends on definitions:  df-bi 185  df-ex 1592  df-nf 1595

This theorem is referenced by:  hbimd  1863  nfand  1867  nfbid  1875  dvelimhw  1897  dvelimf  2044  nfmod2  2286  nfrald  2844  nfifd  3962  nfixp  7480  axrepndlem1  8958  axrepndlem2  8959  axunndlem1  8961  axunnd  8962  axpowndlem2  8964  axpowndlem2OLD  8965  axpowndlem3  8966  axpowndlem3OLD  8967  axpowndlem4  8968  axregndlem2  8971  axregnd  8972  axregndOLD  8973  axinfndlem1  8974  axinfnd  8975  axacndlem4  8979  axacndlem5  8980  axacnd  8981  wl-mo2dnae  29584  wl-mo2t  29585  riotasv2d  33637