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  2474  2euexv  2631  mopick2  2637  2euex  2641  reximd2a  3247  spc2ed  3543  ssrexf  3988  rexdifi  4090  axprlem4OLD  5372  axprlem5OLD  5373  axpowndlem3  10522  axregndlem1  10525  axregnd  10527  dvelimexcased  35219  finminlem  36500  axtcond  36660  difunieq  37690  wl-euequf  37899  pmapglb2xN  40218  unitscyglem5  42638  infrpge  45781  fsumiunss  46005  islpcn  46067  stoweidlem34  46462  stoweidlem35  46463  sge0rpcpnf  46849