![]() |
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 1891. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1778 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1890. (Revised by Wolf Lammen, 10-Jul-2022.) |
Ref | Expression |
---|---|
nfimd.1 | ⊢ (𝜑 → Ⅎ𝑥𝜓) |
nfimd.2 | ⊢ (𝜑 → Ⅎ𝑥𝜒) |
Ref | Expression |
---|---|
nfimd | ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.35 1872 | . . . 4 ⊢ (∃𝑥(𝜓 → 𝜒) ↔ (∀𝑥𝜓 → ∃𝑥𝜒)) | |
2 | 1 | biimpi 215 | . . 3 ⊢ (∃𝑥(𝜓 → 𝜒) → (∀𝑥𝜓 → ∃𝑥𝜒)) |
3 | nfimd.1 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfrd 1785 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) |
5 | nfimd.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
6 | 5 | nfrd 1785 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒)) |
7 | 4, 6 | imim12d 81 | . . 3 ⊢ (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → (∃𝑥𝜓 → ∀𝑥𝜒))) |
8 | 19.38 1833 | . . 3 ⊢ ((∃𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(𝜓 → 𝜒)) | |
9 | 2, 7, 8 | syl56 36 | . 2 ⊢ (𝜑 → (∃𝑥(𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒))) |
10 | 9 | nfd 1784 | 1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1531 ∃wex 1773 Ⅎwnf 1777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 |
This theorem depends on definitions: df-bi 206 df-ex 1774 df-nf 1778 |
This theorem is referenced by: nfimt 1890 nfand 1892 nfbid 1897 nfim1 2184 hbimd 2286 dvelimhw 2333 dvelimf 2439 nfmod2 2544 nfmodv 2545 nfabdw 2918 nfraldw 3298 nfraldwOLD 3310 nfrald 3360 nfifd 4550 nfixpw 8907 nfixp 8908 axrepndlem1 10584 axrepndlem2 10585 axunndlem1 10587 axunnd 10588 axpowndlem2 10590 axpowndlem3 10591 axpowndlem4 10592 axregndlem2 10595 axregnd 10596 axinfndlem1 10597 axinfnd 10598 axacndlem4 10602 axacndlem5 10603 axacnd 10604 bj-dvelimdv 36221 wl-mo2df 36929 wl-mo2t 36934 riotasv2d 38321 nfintd 47930 |
Copyright terms: Public domain | W3C validator |