![]() |
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 1894. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1781 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1893. (Revised by Wolf Lammen, 10-Jul-2022.) |
Ref | Expression |
---|---|
nfimd.1 | ⊢ (𝜑 → Ⅎ𝑥𝜓) |
nfimd.2 | ⊢ (𝜑 → Ⅎ𝑥𝜒) |
Ref | Expression |
---|---|
nfimd | ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.35 1875 | . . . 4 ⊢ (∃𝑥(𝜓 → 𝜒) ↔ (∀𝑥𝜓 → ∃𝑥𝜒)) | |
2 | 1 | biimpi 216 | . . 3 ⊢ (∃𝑥(𝜓 → 𝜒) → (∀𝑥𝜓 → ∃𝑥𝜒)) |
3 | nfimd.1 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
4 | 3 | nfrd 1788 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) |
5 | nfimd.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
6 | 5 | nfrd 1788 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒)) |
7 | 4, 6 | imim12d 81 | . . 3 ⊢ (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → (∃𝑥𝜓 → ∀𝑥𝜒))) |
8 | 19.38 1836 | . . 3 ⊢ ((∃𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(𝜓 → 𝜒)) | |
9 | 2, 7, 8 | syl56 36 | . 2 ⊢ (𝜑 → (∃𝑥(𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒))) |
10 | 9 | nfd 1787 | 1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 ∃wex 1776 Ⅎwnf 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 |
This theorem depends on definitions: df-bi 207 df-ex 1777 df-nf 1781 |
This theorem is referenced by: nfimt 1893 nfand 1895 nfbid 1900 nfim1 2197 hbimd 2297 dvelimhw 2346 dvelimf 2451 nfmod2 2556 nfmodv 2557 nfabdw 2925 nfraldw 3307 nfrald 3370 nfifd 4560 nfixpw 8955 nfixp 8956 axrepndlem1 10630 axrepndlem2 10631 axunndlem1 10633 axunnd 10634 axpowndlem2 10636 axpowndlem3 10637 axpowndlem4 10638 axregndlem2 10641 axregnd 10642 axinfndlem1 10643 axinfnd 10644 axacndlem4 10648 axacndlem5 10649 axacnd 10650 bj-dvelimdv 36834 wl-mo2df 37551 wl-mo2t 37556 riotasv2d 38939 nfintd 48904 |
Copyright terms: Public domain | W3C validator |