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 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 1913  ax-6 1971  ax-7 2011  ax-12 2171

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

This theorem is referenced by:  exlimd  2211  19.41  2228  2ax6elem  2468  2euexv  2626  mopick2  2632  2euex  2636  reximd2a  3250  spc2ed  3561  ssrexf  4013  rexdifi  4110  axprlem4  5386  axprlem5  5387  axpowndlem3  10544  axregndlem1  10547  axregnd  10549  padct  31704  finminlem  34866  difunieq  35918  wl-euequf  36102  pmapglb2xN  38308  infrpge  43706  fsumiunss  43936  islpcn  44000  stoweidlem34  44395  stoweidlem35  44396  sge0rpcpnf  44782