Theorem eximd 2210

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

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  2470  2euexv  2628  mopick2  2634  2euex  2638  reximd2a  3267  spc2ed  3592  ssrexf  4049  rexdifi  4146  axprlem4  5425  axprlem5  5426  axpowndlem3  10594  axregndlem1  10597  axregnd  10599  padct  31944  finminlem  35203  difunieq  36255  wl-euequf  36439  pmapglb2xN  38643  infrpge  44061  fsumiunss  44291  islpcn  44355  stoweidlem34  44750  stoweidlem35  44751  sge0rpcpnf  45137