![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > nfimd | Unicode version |
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.) |
Ref | Expression |
---|---|
nfimd.1 | |
nfimd.2 |
Ref | Expression |
---|---|
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 |
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 |