|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > eximd | Structured version Visualization version GIF version | ||
| Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1833. (Contributed by NM, 29-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) | 
| Ref | Expression | 
|---|---|
| eximd.1 | ⊢ Ⅎ𝑥𝜑 | 
| eximd.2 | ⊢ (𝜑 → (𝜓 → 𝜒)) | 
| Ref | Expression | 
|---|---|
| eximd | ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | eximd.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
| 2 | 1 | nf5ri 2194 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | 
| 3 | eximd.2 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 4 | 2, 3 | eximdh 1863 | 1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∃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 ax-5 1909 ax-6 1966 ax-7 2006 ax-12 2176 | 
| This theorem depends on definitions: df-bi 207 df-ex 1779 df-nf 1783 | 
| This theorem is referenced by: exlimd 2217 19.41 2234 2ax6elem 2474 2euexv 2630 mopick2 2636 2euex 2640 reximd2a 3268 spc2ed 3600 ssrexf 4049 rexdifi 4149 axprlem4OLD 5428 axprlem5OLD 5429 axpowndlem3 10640 axregndlem1 10643 axregnd 10645 padct 32732 dvelimexcased 35092 finminlem 36320 difunieq 37376 wl-euequf 37576 pmapglb2xN 39775 unitscyglem5 42201 infrpge 45367 fsumiunss 45595 islpcn 45659 stoweidlem34 46054 stoweidlem35 46055 sge0rpcpnf 46441 | 
| Copyright terms: Public domain | W3C validator |