Theorem eximd 2253

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 2232	. 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  2255  19.41  2272  2ax6elem  2500  2euexv  2657  mopick2  2663  2euex  2667  reximd2a  3273  spc2ed  3556  ssrexf  3998  rexdifi  4097  axpowndlem3  10684  axregndlem1  10687  axregnd  10689  dvelimexcased  35707  axpowg3  35816  finminlem  37106  axtcond  37266  difunieq  38297  wl-euequf  38506  pmapglb2xN  40829  unitscyglem5  43249  infrpge  46362  fsumiunss  46586  islpcn  46648  stoweidlem34  47043  stoweidlem35  47044  sge0rpcpnf  47430