Theorem eximd 2214

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 2193	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		eximd.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	eximdh 1865	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 1911  ax-6 1970  ax-7 2015  ax-12 2175

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

This theorem is referenced by:  exlimd  2216  19.41  2235  2ax6elem  2482  2euexv  2693  mopick2  2699  2euex  2703  reximd2a  3271  spc2ed  3550  ssrexf  3979  rexdifi  4073  axprlem4  5292  axprlem5  5293  axpowndlem3  10010  axregndlem1  10013  axregnd  10015  padct  30481  finminlem  33779  difunieq  34791  wl-euequf  34975  pmapglb2xN  37068  infrpge  41983  fsumiunss  42217  islpcn  42281  stoweidlem34  42676  stoweidlem35  42677  sge0rpcpnf  43060