![]() |
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 1831. (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 2193 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | eximd.2 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
4 | 2, 3 | eximdh 1862 | 1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃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 ax-5 1908 ax-6 1965 ax-7 2005 ax-12 2175 |
This theorem depends on definitions: df-bi 207 df-ex 1777 df-nf 1781 |
This theorem is referenced by: exlimd 2216 19.41 2233 2ax6elem 2473 2euexv 2629 mopick2 2635 2euex 2639 reximd2a 3267 spc2ed 3601 ssrexf 4062 rexdifi 4160 axprlem4OLD 5435 axprlem5OLD 5436 axpowndlem3 10637 axregndlem1 10640 axregnd 10642 padct 32737 dvelimexcased 35070 finminlem 36301 difunieq 37357 wl-euequf 37555 pmapglb2xN 39755 unitscyglem5 42181 infrpge 45301 fsumiunss 45531 islpcn 45595 stoweidlem34 45990 stoweidlem35 45991 sge0rpcpnf 46377 |
Copyright terms: Public domain | W3C validator |