Theorem nfimd 1823

Description: If in a context x is not free in ps and ch, it is not free in ( ps -> ch ). Deduction form of nfimt 1821. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1710 changed. (Revised by Wolf Lammen, 18-Sep-2021.)

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		nfimt2 1822	. 2 |- ( ( F/ x ps /\ F/ x ch ) -> F/ x ( ps -> ch ) )
4	1, 2, 3	syl2anc 693	1 |- ( ph -> F/ x ( ps -> ch ) )

Syntax hints:   -> wi 4   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-nf 1710

This theorem is referenced by:  nfand  1826  nfbid  1832  nfim1  2067  hbimd  2126  dvelimhw  2173  dvelimf  2334  nfmod2  2483  nfrald  2944  nfifd  4114  nfixp  7927  axrepndlem1  9414  axrepndlem2  9415  axunndlem1  9417  axunnd  9418  axpowndlem2  9420  axpowndlem3  9421  axpowndlem4  9422  axregndlem2  9425  axregnd  9426  axinfndlem1  9427  axinfnd  9428  axacndlem4  9432  axacndlem5  9433  axacnd  9434  bj-dvelimdv  32834  wl-mo2df  33352  wl-mo2t  33357  riotasv2d  34243  nfintd  42420