Theorem eximd 2254

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

Syntax hints:   → wi 4  ∃wex 1802  Ⅎwnf 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-ex 1803  df-nf 1807

This theorem is referenced by:  exlimd  2256  19.41  2273  2ax6elem  2504  2euexv  2661  mopick2  2667  2euex  2671  reximd2a  3275  spc2ed  3563  ssrexf  4006  rexdifi  4106  axprlem4OLD  5392  axprlem5OLD  5393  axpowndlem3  10572  axregndlem1  10575  axregnd  10577  dvelimexcased  35382  axpowg3  35456  finminlem  36691  axtcond  36851  difunieq  37880  wl-euequf  38089  pmapglb2xN  40408  unitscyglem5  42828  infrpge  45925  fsumiunss  46149  islpcn  46211  stoweidlem34  46606  stoweidlem35  46607  sge0rpcpnf  46993