Theorem eximd 2228

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

Syntax hints:   → wi 4  ∃wex 1786  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-nf 1791

This theorem is referenced by:  exlimd  2230  19.41  2247  2ax6elem  2478  2euexv  2635  mopick2  2641  2euex  2645  reximd2a  3249  spc2ed  3539  ssrexf  3981  rexdifi  4080  axprlem4OLD  5359  axprlem5OLD  5360  axpowndlem3  10513  axregndlem1  10516  axregnd  10518  dvelimexcased  35259  axpowg3  35329  finminlem  36546  axtcond  36706  difunieq  37736  wl-euequf  37945  pmapglb2xN  40264  unitscyglem5  42684  infrpge  45796  fsumiunss  46020  islpcn  46082  stoweidlem34  46477  stoweidlem35  46478  sge0rpcpnf  46864