Theorem eximd 2252

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  exlimd  2254  19.41  2271  2ax6elem  2499  2euexv  2656  mopick2  2662  2euex  2666  reximd2a  3272  spc2ed  3555  ssrexf  3998  rexdifi  4097  axprlem4OLD  5395  axprlem5OLD  5396  axpowndlem3  10609  axregndlem1  10612  axregnd  10614  dvelimexcased  35587  axpowg3  35675  finminlem  36938  axtcond  37098  difunieq  38129  wl-euequf  38338  pmapglb2xN  40646  unitscyglem5  43066  infrpge  46182  fsumiunss  46406  islpcn  46468  stoweidlem34  46863  stoweidlem35  46864  sge0rpcpnf  47250