Theorem eximd 2217

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

Syntax hints:   → wi 4  ∃wex 1779  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  exlimd  2219  19.41  2236  2ax6elem  2468  2euexv  2624  mopick2  2630  2euex  2634  reximd2a  3245  spc2ed  3564  ssrexf  4010  rexdifi  4109  axprlem4OLD  5379  axprlem5OLD  5380  axpowndlem3  10528  axregndlem1  10531  axregnd  10533  padct  32693  dvelimexcased  35060  finminlem  36299  difunieq  37355  wl-euequf  37555  pmapglb2xN  39759  unitscyglem5  42180  infrpge  45340  fsumiunss  45566  islpcn  45630  stoweidlem34  46025  stoweidlem35  46026  sge0rpcpnf  46412