MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfimd Unicode version

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
StepHypRef Expression
1 nfimd.1 . 2
2 nfimd.2 . 2
3 nfnf1 1899 . . . 4
4 nfnf1 1899 . . . 4
5 nfr 1873 . . . . . 6
65imim2d 52 . . . . 5
7 19.21t 1904 . . . . . 6
87biimprd 223 . . . . 5
96, 8syl9r 72 . . . 4
103, 4, 9alrimd 1881 . . 3
11 df-nf 1617 . . 3
1210, 11syl6ibr 227 . 2
131, 2, 12sylc 60 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator