Theorem eximd 2252

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

Syntax hints:   → wi 4  ∃wex 1809  Ⅎwnf 1813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-ex 1810  df-nf 1814

This theorem is referenced by:  exlimd  2254  19.41  2271  2ax6elem  2502  2euexv  2659  mopick2  2665  2euex  2669  reximd2a  3275  spc2ed  3560  ssrexf  4004  rexdifi  4104  axprlem4OLD  5401  axprlem5OLD  5402  axpowndlem3  10579  axregndlem1  10582  axregnd  10584  dvelimexcased  35465  axpowg3  35561  finminlem  36849  axtcond  37009  difunieq  38040  wl-euequf  38249  pmapglb2xN  40566  unitscyglem5  42986  infrpge  46087  fsumiunss  46311  islpcn  46373  stoweidlem34  46768  stoweidlem35  46769  sge0rpcpnf  47155