Theorem nfimd 1925

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 1907	. . . 4 |- F/ x F/ x ps
4		nfnf1 1907	. . . 4 |- F/ x F/ x ch
5		nfr 1881	. . . . . 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 1912	. . . . . 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 1889	. . 3 |- ( F/ x ps -> ( F/ x ch -> A. x ( ( ps -> ch ) -> A. x ( ps -> ch ) ) ) )
11		df-nf 1625	. . 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 1397   F/wnf 1624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-12 1862

This theorem depends on definitions:  df-bi 185  df-ex 1621  df-nf 1625

This theorem is referenced by:  hbimd  1929  nfand  1933  nfbid  1941  dvelimhw  1963  dvelimf  2082  nfmod2  2233  nfrald  2767  nfifd  3885  nfixp  7407  axrepndlem1  8880  axrepndlem2  8881  axunndlem1  8883  axunnd  8884  axpowndlem2  8886  axpowndlem3  8887  axpowndlem4  8888  axregndlem2  8891  axregnd  8892  axregndOLD  8893  axinfndlem1  8894  axinfnd  8895  axacndlem4  8899  axacndlem5  8900  axacnd  8901  wl-mo2dnae  30184  wl-mo2t  30185  riotasv2d  35101