Theorem eximd 2215

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

Syntax hints:   → wi 4  ∃wex 1778  Ⅎwnf 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-ex 1779  df-nf 1783

This theorem is referenced by:  exlimd  2217  19.41  2234  2ax6elem  2473  2euexv  2629  mopick2  2635  2euex  2639  reximd2a  3255  spc2ed  3584  ssrexf  4030  rexdifi  4130  axprlem4OLD  5409  axprlem5OLD  5410  axpowndlem3  10621  axregndlem1  10624  axregnd  10626  padct  32667  dvelimexcased  35066  finminlem  36294  difunieq  37350  wl-euequf  37550  pmapglb2xN  39749  unitscyglem5  42175  infrpge  45334  fsumiunss  45562  islpcn  45626  stoweidlem34  46021  stoweidlem35  46022  sge0rpcpnf  46408