Theorem eximd 2224

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

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

This theorem is referenced by:  exlimd  2226  19.41  2243  2ax6elem  2475  2euexv  2632  mopick2  2638  2euex  2642  reximd2a  3248  spc2ed  3544  ssrexf  3989  rexdifi  4091  axprlem4OLD  5368  axprlem5OLD  5369  axpowndlem3  10516  axregndlem1  10519  axregnd  10521  dvelimexcased  35238  finminlem  36519  axtcond  36679  difunieq  37707  wl-euequf  37916  pmapglb2xN  40235  unitscyglem5  42655  infrpge  45802  fsumiunss  46026  islpcn  46088  stoweidlem34  46483  stoweidlem35  46484  sge0rpcpnf  46870