![]() |
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 1837. (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 2189 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | eximd.2 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
4 | 2, 3 | eximdh 1868 | 1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1782 Ⅎwnf 1786 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-ex 1783 df-nf 1787 |
This theorem is referenced by: exlimd 2212 19.41 2229 2ax6elem 2469 2euexv 2632 mopick2 2638 2euex 2642 reximd2a 3255 spc2ed 3563 ssrexf 4013 rexdifi 4110 axprlem4 5386 axprlem5 5387 axpowndlem3 10542 axregndlem1 10545 axregnd 10547 padct 31678 finminlem 34819 difunieq 35874 wl-euequf 36058 pmapglb2xN 38264 infrpge 43659 fsumiunss 43890 islpcn 43954 stoweidlem34 44349 stoweidlem35 44350 sge0rpcpnf 44736 |
Copyright terms: Public domain | W3C validator |