Theorem eximd 2255

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 2234	. 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 2216

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

This theorem is used by:  exlimd  2257  19.41  2274  2ax6elem  2504  2euexv  2661  mopick2  2667  2euex  2671  reximd2a  3277  spc2ed  3562  ssrexf  4005  rexdifi  4104  axprlem4OLD  5403  axprlem5OLD  5404  axpowndlem3  10601  axregndlem1  10604  axregnd  10606  dvelimexcased  35532  axpowg3  35620  finminlem  36888  axtcond  37048  difunieq  38079  wl-euequf  38288  pmapglb2xN  40606  unitscyglem5  43026  infrpge  46127  fsumiunss  46351  islpcn  46413  stoweidlem34  46808  stoweidlem35  46809  sge0rpcpnf  47195