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 1825. (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 2185 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | eximd.2 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
4 | 2, 3 | eximdh 1856 | 1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1771 Ⅎwnf 1775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-ex 1772 df-nf 1776 |
This theorem is referenced by: exlimd 2208 19.41 2227 2ax6elem 2485 sbimdOLD 2511 2euexv 2709 mopick2 2715 2euex 2719 reximd2a 3309 spc2ed 3599 ssrexf 4028 rexdifi 4119 axprlem4 5317 axprlem5 5318 axpowndlem3 10009 axregndlem1 10012 axregnd 10014 padct 30381 finminlem 33563 difunieq 34537 wl-euequf 34691 pmapglb2xN 36788 disjinfi 41330 infrpge 41495 fsumiunss 41732 islpcn 41796 stoweidlem34 42196 stoweidlem35 42197 sge0rpcpnf 42580 |
Copyright terms: Public domain | W3C validator |