Theorem eximd 2223

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 2202	. 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 2184

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

This theorem is referenced by:  exlimd  2225  19.41  2242  2ax6elem  2474  2euexv  2631  mopick2  2637  2euex  2641  reximd2a  3246  spc2ed  3555  ssrexf  4000  rexdifi  4102  axprlem4OLD  5374  axprlem5OLD  5375  axpowndlem3  10510  axregndlem1  10513  axregnd  10515  padct  32797  dvelimexcased  35233  finminlem  36512  difunieq  37579  wl-euequf  37779  pmapglb2xN  40032  unitscyglem5  42453  infrpge  45596  fsumiunss  45821  islpcn  45883  stoweidlem34  46278  stoweidlem35  46279  sge0rpcpnf  46665