|   | 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 1895. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1783 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1894. (Revised by Wolf Lammen, 10-Jul-2022.) | 
| Ref | Expression | 
|---|---|
| nfimd.1 | ⊢ (𝜑 → Ⅎ𝑥𝜓) | 
| nfimd.2 | ⊢ (𝜑 → Ⅎ𝑥𝜒) | 
| Ref | Expression | 
|---|---|
| nfimd | ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | 19.35 1876 | . . . 4 ⊢ (∃𝑥(𝜓 → 𝜒) ↔ (∀𝑥𝜓 → ∃𝑥𝜒)) | |
| 2 | 1 | biimpi 216 | . . 3 ⊢ (∃𝑥(𝜓 → 𝜒) → (∀𝑥𝜓 → ∃𝑥𝜒)) | 
| 3 | nfimd.1 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
| 4 | 3 | nfrd 1790 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) | 
| 5 | nfimd.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
| 6 | 5 | nfrd 1790 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜒 → ∀𝑥𝜒)) | 
| 7 | 4, 6 | imim12d 81 | . . 3 ⊢ (𝜑 → ((∀𝑥𝜓 → ∃𝑥𝜒) → (∃𝑥𝜓 → ∀𝑥𝜒))) | 
| 8 | 19.38 1838 | . . 3 ⊢ ((∃𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(𝜓 → 𝜒)) | |
| 9 | 2, 7, 8 | syl56 36 | . 2 ⊢ (𝜑 → (∃𝑥(𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒))) | 
| 10 | 9 | nfd 1789 | 1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∀wal 1537 ∃wex 1778 Ⅎwnf 1782 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 | 
| This theorem depends on definitions: df-bi 207 df-ex 1779 df-nf 1783 | 
| This theorem is referenced by: nfimt 1894 nfand 1896 nfbid 1901 nfim1 2198 hbimd 2297 dvelimhw 2346 dvelimf 2452 nfmod2 2557 nfmodv 2558 nfabdw 2926 nfraldw 3308 nfrald 3371 nfifd 4554 nfixpw 8957 nfixp 8958 axrepndlem1 10633 axrepndlem2 10634 axunndlem1 10636 axunnd 10637 axpowndlem2 10639 axpowndlem3 10640 axpowndlem4 10641 axregndlem2 10644 axregnd 10645 axinfndlem1 10646 axinfnd 10647 axacndlem4 10651 axacndlem5 10652 axacnd 10653 bj-dvelimdv 36853 wl-mo2df 37572 wl-mo2t 37577 riotasv2d 38959 nfintd 49247 | 
| Copyright terms: Public domain | W3C validator |