Theorem eximd 2209

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 2188	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		eximd.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	eximdh 1867	1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  exlimd  2211  19.41  2228  2ax6elem  2470  2euexv  2633  mopick2  2639  2euex  2643  reximd2a  3245  spc2ed  3540  ssrexf  3985  rexdifi  4080  axprlem4  5349  axprlem5  5350  axpowndlem3  10355  axregndlem1  10358  axregnd  10360  padct  31054  finminlem  34507  difunieq  35545  wl-euequf  35729  pmapglb2xN  37786  infrpge  42890  fsumiunss  43116  islpcn  43180  stoweidlem34  43575  stoweidlem35  43576  sge0rpcpnf  43959