![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfimd | Structured version Visualization version GIF version |
Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 → 𝜒). Deduction form of nfim 2001. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1885 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1999. (Revised by Wolf Lammen, 10-Jul-2022.) |
Ref | Expression |
---|---|
nfimd.1 | ⊢ (𝜑 → Ⅎ𝑥𝜓) |
nfimd.2 | ⊢ (𝜑 → Ⅎ𝑥𝜒) |
Ref | Expression |
---|---|
nfimd | ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.35 1982 | . . . 4 ⊢ (∃𝑥(𝜓 → 𝜒) ↔ (∀𝑥𝜓 → ∃𝑥𝜒)) | |
2 | 1 | biimpi 208 | . . 3 ⊢ (∃𝑥(𝜓 → 𝜒) → (∀𝑥𝜓 → ∃𝑥𝜒)) |
3 | nfimd.1 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfrd 1892 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) |
5 | nfimd.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
6 | 5 | nfrd 1892 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒)) |
7 | 4, 6 | imim12d 81 | . . 3 ⊢ (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → (∃𝑥𝜓 → ∀𝑥𝜒))) |
8 | 19.38 1939 | . . 3 ⊢ ((∃𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(𝜓 → 𝜒)) | |
9 | 2, 7, 8 | syl56 36 | . 2 ⊢ (𝜑 → (∃𝑥(𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒))) |
10 | 9 | nfd 1891 | 1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1656 ∃wex 1880 Ⅎwnf 1884 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 |
This theorem depends on definitions: df-bi 199 df-ex 1881 df-nf 1885 |
This theorem is referenced by: nfimt 1999 nfand 2002 nfbid 2007 nfim1 2241 hbimd 2332 dvelimhw 2371 dvelimf 2469 nfmod2 2627 nfmodv 2628 nfmod2OLD 2677 nfrald 3153 nfifd 4334 nfixp 8194 axrepndlem1 9729 axrepndlem2 9730 axunndlem1 9732 axunnd 9733 axpowndlem2 9735 axpowndlem3 9736 axpowndlem4 9737 axregndlem2 9740 axregnd 9741 axinfndlem1 9742 axinfnd 9743 axacndlem4 9747 axacndlem5 9748 axacnd 9749 bj-dvelimdv 33357 wl-mo2df 33896 wl-mo2t 33901 riotasv2d 35032 nfintd 43315 |
Copyright terms: Public domain | W3C validator |