Theorem eximd 2258

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

Syntax hints:   → wi 4  ∃wex 1806  Ⅎwnf 1810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811

This theorem is referenced by:  exlimd  2260  19.41  2277  2ax6elem  2508  2euexv  2665  mopick2  2671  2euex  2675  reximd2a  3281  spc2ed  3569  ssrexf  4012  rexdifi  4112  axprlem4OLD  5402  axprlem5OLD  5403  axpowndlem3  10583  axregndlem1  10586  axregnd  10588  dvelimexcased  35409  axpowg3  35483  finminlem  36717  axtcond  36877  difunieq  37907  wl-euequf  38116  pmapglb2xN  40435  unitscyglem5  42855  infrpge  45958  fsumiunss  46182  islpcn  46244  stoweidlem34  46639  stoweidlem35  46640  sge0rpcpnf  47026