Theorem nfimd 1917

Description: If in a context is not free in and , it is not free in . (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)

Hypotheses

Ref	Expression
nfimd.1
nfimd.2

Assertion

Ref	Expression
nfimd

Proof of Theorem nfimd

Step	Hyp	Ref	Expression
1		nfimd.1	. 2
2		nfimd.2	. 2
3		nfnf1 1899	. . . 4
4		nfnf1 1899	. . . 4
5		nfr 1873	. . . . . 6
6	5	imim2d 52	. . . . 5
7		19.21t 1904	. . . . . 6
8	7	biimprd 223	. . . . 5
9	6, 8	syl9r 72	. . . 4
10	3, 4, 9	alrimd 1881	. . 3
11		df-nf 1617	. . 3
12	10, 11	syl6ibr 227	. 2
13	1, 2, 12	sylc 60	1

Syntax hints:  ->wi 4  A.wal 1393  F/wnf 1616

This theorem is referenced by:  hbimd  1921  nfand  1925  nfbid  1933  dvelimhw  1955  dvelimf  2076  nfmod2  2297  nfrald  2842  nfifd  3969  nfixp  7508  axrepndlem1  8988  axrepndlem2  8989  axunndlem1  8991  axunnd  8992  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem3  8996  axpowndlem3OLD  8997  axpowndlem4  8998  axregndlem2  9001  axregnd  9002  axregndOLD  9003  axinfndlem1  9004  axinfnd  9005  axacndlem4  9009  axacndlem5  9010  axacnd  9011  wl-mo2dnae  30019  wl-mo2t  30020  riotasv2d  34688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617