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 1785 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 218 | . . 3 ⊢ (∃𝑥(𝜓 → 𝜒) → (∀𝑥𝜓 → ∃𝑥𝜒)) |
3 | nfimd.1 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfrd 1792 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) |
5 | nfimd.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
6 | 5 | nfrd 1792 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒)) |
7 | 4, 6 | imim12d 81 | . . 3 ⊢ (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → (∃𝑥𝜓 → ∀𝑥𝜒))) |
8 | 19.38 1839 | . . 3 ⊢ ((∃𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(𝜓 → 𝜒)) | |
9 | 2, 7, 8 | syl56 36 | . 2 ⊢ (𝜑 → (∃𝑥(𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒))) |
10 | 9 | nfd 1791 | 1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 ∃wex 1780 Ⅎwnf 1784 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 |
This theorem depends on definitions: df-bi 209 df-ex 1781 df-nf 1785 |
This theorem is referenced by: nfimt 1896 nfand 1898 nfbid 1903 nfim1 2199 hbimd 2306 dvelimhw 2366 dvelimf 2470 nfmod2 2642 nfmodv 2643 nfraldw 3225 nfrald 3226 nfifd 4497 nfixpw 8482 nfixp 8483 axrepndlem1 10016 axrepndlem2 10017 axunndlem1 10019 axunnd 10020 axpowndlem2 10022 axpowndlem3 10023 axpowndlem4 10024 axregndlem2 10027 axregnd 10028 axinfndlem1 10029 axinfnd 10030 axacndlem4 10034 axacndlem5 10035 axacnd 10036 bj-dvelimdv 34177 wl-mo2df 34808 wl-mo2t 34813 riotasv2d 36095 nfintd 44783 |
Copyright terms: Public domain | W3C validator |