Theorem eximd 2221

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

Syntax hints:   → wi 4  ∃wex 1780  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  exlimd  2223  19.41  2240  2ax6elem  2472  2euexv  2629  mopick2  2635  2euex  2639  reximd2a  3244  spc2ed  3553  ssrexf  3998  rexdifi  4100  axprlem4OLD  5372  axprlem5OLD  5373  axpowndlem3  10508  axregndlem1  10511  axregnd  10513  padct  32746  dvelimexcased  35182  finminlem  36461  difunieq  37518  wl-euequf  37718  pmapglb2xN  39971  unitscyglem5  42392  infrpge  45538  fsumiunss  45763  islpcn  45825  stoweidlem34  46220  stoweidlem35  46221  sge0rpcpnf  46607