Theorem eximii 1839

Description: Inference associated with eximi 1837. (Contributed by BJ, 3-Feb-2018.)

Hypotheses

Ref	Expression
eximii.1	⊢ ∃𝑥𝜑
eximii.2	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
eximii	⊢ ∃𝑥𝜓

Proof of Theorem eximii

Step	Hyp	Ref	Expression
1		eximii.1	. 2 ⊢ ∃𝑥𝜑
2		eximii.2	. . 3 ⊢ (𝜑 → 𝜓)
3	2	eximi 1837	. 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
4	1, 3	ax-mp 5	1 ⊢ ∃𝑥𝜓

Syntax hints:   → wi 4  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  exan  1865  ax6evr  2018  spimedv  2190  spimfv  2232  ax6e  2383  spim  2387  spimed  2388  spimvALT  2391  spei  2394  equvini  2455  equvel  2456  euequ  2597  dariiALT  2667  barbariALT  2671  festinoALT  2676  barocoALT  2678  daraptiALT  2686  vtoclf  3497  axrep2  5212  axnul  5229  nalset  5237  notzfaus  5285  elALT2  5292  dtruALT2  5293  dvdemo1  5296  dvdemo2  5297  eusv2nf  5318  axprALT  5345  axpr  5351  dtru  5359  inf1  9380  bnd  9650  axpowndlem2  10354  grothomex  10585  tgjustc1  26836  tgjustc2  26837  bnj101  32702  axextdfeq  33773  ax8dfeq  33774  axextndbi  33780  snelsingles  34224  bj-ax6elem2  34848  bj-dtru  34999  ax6er  35016  bj-vtoclf  35100  wl-exeq  35693  sn-el  40187  spd  46384  elpglem2  46417  eximp-surprise2  46489