Theorem eximd 2217

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782

This theorem is referenced by:  exlimd  2219  19.41  2236  2ax6elem  2478  2euexv  2634  mopick2  2640  2euex  2644  reximd2a  3275  spc2ed  3614  ssrexf  4075  rexdifi  4173  axprlem4  5444  axprlem5  5445  axpowndlem3  10668  axregndlem1  10671  axregnd  10673  padct  32733  dvelimexcased  35053  finminlem  36284  difunieq  37340  wl-euequf  37528  pmapglb2xN  39729  unitscyglem5  42156  infrpge  45266  fsumiunss  45496  islpcn  45560  stoweidlem34  45955  stoweidlem35  45956  sge0rpcpnf  46342