Theorem eximd 2256

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 2235	. 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 1945  ax-6 2002  ax-7 2043  ax-12 2216

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

This theorem is used by:  exlimd  2258  19.41  2275  2ax6elem  2502  2euexv  2659  mopick2  2665  2euex  2669  reximd2a  3276  spc2ed  3559  ssrexf  3980  rexdifi  4089  axpowndlem3  10723  axregndlem1  10726  axregnd  10728  dvelimexcased  35818  rmo6  35821  axpowg3  35957  finminlem  37321  axtcond  37481  difunieq  38565  wl-euequf  38774  pmapglb2xN  41095  unitscyglem5  43515  infrpge  46636  fsumiunss  46860  islpcn  46922  stoweidlem34  47317  stoweidlem35  47318  sge0rpcpnf  47704