Theorem eximd 2219

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1835. (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 2198	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		eximd.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	eximdh 1865	1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Syntax hints:   → wi 4  ∃wex 1780  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  exlimd  2221  19.41  2238  2ax6elem  2470  2euexv  2626  mopick2  2632  2euex  2636  reximd2a  3242  spc2ed  3551  ssrexf  3996  rexdifi  4097  axprlem4OLD  5365  axprlem5OLD  5366  axpowndlem3  10490  axregndlem1  10493  axregnd  10495  padct  32701  dvelimexcased  35089  finminlem  36360  difunieq  37416  wl-euequf  37616  pmapglb2xN  39819  unitscyglem5  42240  infrpge  45398  fsumiunss  45623  islpcn  45685  stoweidlem34  46080  stoweidlem35  46081  sge0rpcpnf  46467