Theorem eximd 2252

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1866. (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 1896	1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

This proof depends on syntax axioms:   → wi 4  ∃wex 1811  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816

This theorem is used by:  exlimd  2254  19.41  2271  2ax6elem  2499  2euexv  2656  mopick2  2662  2euex  2666  reximd2a  3272  spc2ed  3555  ssrexf  3976  rexdifi  4085  axpowndlem3  10691  axregndlem1  10694  axregnd  10696  dvelimexcased  35757  rmo6  35760  axpowg3  35884  finminlem  37230  axtcond  37390  difunieq  38434  wl-euequf  38643  pmapglb2xN  40966  unitscyglem5  43386  infrpge  46499  fsumiunss  46723  islpcn  46785  stoweidlem34  47180  stoweidlem35  47181  sge0rpcpnf  47567