Theorem eximd 2215

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.)

Hypotheses

Ref	Expression
eximd.1	⊢ Ⅎ𝑥𝜑
eximd.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
eximd	⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Proof of Theorem eximd

Step	Hyp	Ref	Expression
1		eximd.1	. . 3 ⊢ Ⅎ𝑥𝜑
2	1	nf5ri 2194	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		eximd.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	eximdh 1863	1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

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