Theorem eximd 2215

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1833. (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 2194	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		eximd.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	eximdh 1864	1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Syntax hints:   → wi 4  ∃wex 1779  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-12 2176

This theorem depends on definitions:  df-bi 209  df-ex 1780  df-nf 1784

This theorem is referenced by:  exlimd  2217  19.41  2236  2ax6elem  2492  sbimdOLD  2517  2euexv  2715  mopick2  2721  2euex  2725  reximd2a  3315  spc2ed  3605  ssrexf  4034  rexdifi  4125  axprlem4  5330  axprlem5  5331  axpowndlem3  10024  axregndlem1  10027  axregnd  10029  padct  30458  finminlem  33670  difunieq  34659  wl-euequf  34814  pmapglb2xN  36912  disjinfi  41460  infrpge  41625  fsumiunss  41862  islpcn  41926  stoweidlem34  42326  stoweidlem35  42327  sge0rpcpnf  42710