![]() |
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 1897. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1786 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1896. (Revised by Wolf Lammen, 10-Jul-2022.) |
Ref | Expression |
---|---|
nfimd.1 | ⊢ (𝜑 → Ⅎ𝑥𝜓) |
nfimd.2 | ⊢ (𝜑 → Ⅎ𝑥𝜒) |
Ref | Expression |
---|---|
nfimd | ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.35 1878 | . . . 4 ⊢ (∃𝑥(𝜓 → 𝜒) ↔ (∀𝑥𝜓 → ∃𝑥𝜒)) | |
2 | 1 | biimpi 219 | . . 3 ⊢ (∃𝑥(𝜓 → 𝜒) → (∀𝑥𝜓 → ∃𝑥𝜒)) |
3 | nfimd.1 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfrd 1793 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) |
5 | nfimd.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
6 | 5 | nfrd 1793 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒)) |
7 | 4, 6 | imim12d 81 | . . 3 ⊢ (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → (∃𝑥𝜓 → ∀𝑥𝜒))) |
8 | 19.38 1840 | . . 3 ⊢ ((∃𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(𝜓 → 𝜒)) | |
9 | 2, 7, 8 | syl56 36 | . 2 ⊢ (𝜑 → (∃𝑥(𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒))) |
10 | 9 | nfd 1792 | 1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1536 ∃wex 1781 Ⅎwnf 1785 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 |
This theorem depends on definitions: df-bi 210 df-ex 1782 df-nf 1786 |
This theorem is referenced by: nfimt 1896 nfand 1898 nfbid 1903 nfim1 2197 hbimd 2302 dvelimhw 2355 dvelimf 2459 nfmod2 2617 nfmodv 2618 nfraldw 3187 nfrald 3188 nfifd 4453 nfixpw 8463 nfixp 8464 axrepndlem1 10003 axrepndlem2 10004 axunndlem1 10006 axunnd 10007 axpowndlem2 10009 axpowndlem3 10010 axpowndlem4 10011 axregndlem2 10014 axregnd 10015 axinfndlem1 10016 axinfnd 10017 axacndlem4 10021 axacndlem5 10022 axacnd 10023 bj-dvelimdv 34290 wl-mo2df 34971 wl-mo2t 34976 riotasv2d 36253 nfintd 45203 |
Copyright terms: Public domain | W3C validator |