Theorem eximd 2251

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

Syntax hints:   → wi 4  ∃wex 1799  Ⅎwnf 1803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-12 2212

This theorem depends on definitions:  df-bi 209  df-ex 1800  df-nf 1804

This theorem is referenced by:  exlimd  2253  19.41  2270  2ax6elem  2501  2euexv  2658  mopick2  2664  2euex  2668  reximd2a  3272  spc2ed  3560  ssrexf  4003  rexdifi  4103  axprlem4OLD  5387  axprlem5OLD  5388  axpowndlem3  10557  axregndlem1  10560  axregnd  10562  dvelimexcased  35372  axpowg3  35444  finminlem  36678  axtcond  36838  difunieq  37868  wl-euequf  38077  pmapglb2xN  40396  unitscyglem5  42816  infrpge  45927  fsumiunss  46151  islpcn  46213  stoweidlem34  46608  stoweidlem35  46609  sge0rpcpnf  46995