Theorem nfimd 2010

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 1991	. . . 4 |- F/ x F/ x ps
4		nfnf1 1991	. . . 4 |- F/ x F/ x ch
5		nfr 1961	. . . . . 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 1996	. . . . . 6 |- ( F/ x ps -> ( A. x ( ps -> ch ) <-> ( ps -> A. x ch ) ) )
8	7	biimprd 231	. . . . 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 1969	. . 3 |- ( F/ x ps -> ( F/ x ch -> A. x ( ( ps -> ch ) -> A. x ( ps -> ch ) ) ) )
11		df-nf 1678	. . 3 |- ( F/ x ( ps -> ch ) <-> A. x ( ( ps -> ch ) -> A. x ( ps -> ch ) ) )
12	10, 11	syl6ibr 235	. 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 1452   F/wnf 1677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-12 1943

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1674  df-nf 1678

This theorem is referenced by:  hbimd  2014  nfand  2018  nfbid  2026  dvelimhw  2070  dvelimf  2178  nfmod2  2322  nfrald  2784  nfifd  3920  nfixp  7566  axrepndlem1  9042  axrepndlem2  9043  axunndlem1  9045  axunnd  9046  axpowndlem2  9048  axpowndlem3  9049  axpowndlem4  9050  axregndlem2  9053  axregnd  9054  axinfndlem1  9055  axinfnd  9056  axacndlem4  9060  axacndlem5  9061  axacnd  9062  wl-mo2df  31943  wl-mo2t  31948  riotasv2d  32573