Theorem eximd 2212

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

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 2191	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		eximd.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	eximdh 1868	1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Syntax hints:   → wi 4  ∃wex 1783  Ⅎwnf 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-nf 1788

This theorem is referenced by:  exlimd  2214  19.41  2231  2ax6elem  2470  2euexv  2633  mopick2  2639  2euex  2643  reximd2a  3240  spc2ed  3530  ssrexf  3981  rexdifi  4076  axprlem4  5344  axprlem5  5345  axpowndlem3  10286  axregndlem1  10289  axregnd  10291  padct  30956  finminlem  34434  difunieq  35472  wl-euequf  35656  pmapglb2xN  37713  infrpge  42780  fsumiunss  43006  islpcn  43070  stoweidlem34  43465  stoweidlem35  43466  sge0rpcpnf  43849