Theorem eximd 2201

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

Syntax hints:   → wi 4  ∃wex 1773  Ⅎwnf 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2163

This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778

This theorem is referenced by:  exlimd  2203  19.41  2220  2ax6elem  2461  2euexv  2619  mopick2  2625  2euex  2629  reximd2a  3258  spc2ed  3583  ssrexf  4041  rexdifi  4138  axprlem4  5415  axprlem5  5416  axpowndlem3  10591  axregndlem1  10594  axregnd  10596  padct  32416  finminlem  35694  difunieq  36746  wl-euequf  36933  pmapglb2xN  39137  infrpge  44571  fsumiunss  44801  islpcn  44865  stoweidlem34  45260  stoweidlem35  45261  sge0rpcpnf  45647