Theorem nfimd 1808

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/xps)
nfimd.2	|- (ph -> F/xch)

Assertion

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

Proof of Theorem nfimd

Step	Hyp	Ref	Expression
1		nfimd.1	. 2 |- (ph -> F/xps)
2		nfimd.2	. 2 |- (ph -> F/xch)
3		nfnf1 1790	. . . 4 |- F/x F/xps
4		nfnf1 1790	. . . 4 |- F/x F/xch
5		nfr 1761	. . . . . 6 |- ( F/xch -> (ch -> A.xch))
6	5	imim2d 48	. . . . 5 |- ( F/xch -> ((ps -> ch) -> (ps -> A.xch)))
7		19.21t 1795	. . . . . 6 |- ( F/xps -> (A.x(ps -> ch) <-> (ps -> A.xch)))
8	7	biimprd 214	. . . . 5 |- ( F/xps -> ((ps -> A.xch) -> A.x(ps -> ch)))
9	6, 8	syl9r 67	. . . 4 |- ( F/xps -> ( F/xch -> ((ps -> ch) -> A.x(ps -> ch))))
10	3, 4, 9	alrimd 1769	. . 3 |- ( F/xps -> ( F/xch -> A.x((ps -> ch) -> A.x(ps -> ch))))
11		df-nf 1545	. . 3 |- ( F/x(ps -> ch) <-> A.x((ps -> ch) -> A.x(ps -> ch)))
12	10, 11	syl6ibr 218	. 2 |- ( F/xps -> ( F/xch -> F/x(ps -> ch)))
13	1, 2, 12	sylc 56	1 |- (ph -> F/x(ps -> ch))

Syntax hints:   -> wi 4  A.wal 1540   F/wnf 1544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545

This theorem is referenced by:  nfimOLD  1814  hbimd  1815  19.23tOLD  1819  nfand  1822  nfbid  1832  nfbidOLD  1833  nfnfOLD  1846  19.21tOLD  1863  dvelimf  1997  nfsb4t  2080  nfmod2  2217  nfrald  2666  nfifd  3686