Theorem eximii 1870

Description: Inference associated with eximi 1868. (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 1868	. 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
4	1, 3	ax-mp 5	1 ⊢ ∃𝑥𝜓

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  exan  1895  ax6evr  2050  spimedv  2237  spimfv  2279  ax6e  2415  spim  2419  spimed  2420  spimvALT  2423  spei  2426  equvini  2487  equvel  2488  euequ  2625  dariiALT  2693  barbariALT  2697  festinoALT  2702  barocoALT  2704  daraptiALT  2712  ceqsexv2d  3503  axrep2  5241  axnul  5265  exnelv  5273  nalsetOLD  5275  notsep  5332  axpow3  5337  elALT2  5338  dtruALT2  5339  dvdemo1  5342  dvdemo2  5343  eusv2nf  5364  axprALT  5391  axprlem1  5392  exel  5409  el  5413  relopabi  5809  uniex2  7786  elirrvOLD  9629  inf1  9660  omex  9681  bnd  9992  axpowndlem2  10722  grothomex  10953  tgjustc1  28994  tgjustc2  28995  bnj101  35465  axnulALT3  35856  axprALT2  35857  axsepg2  35949  axsepg3  35950  axsepg3ALT  35951  axsepg4  35952  axpowg2  35956  axpowg3  35957  axextdfeq  36774  ax8dfeq  36775  axextndbi  36781  snelsingles  36899  axtco  37474  axtco2  37477  axuntco  37482  elALTtco  37484  tz9.1tco  37486  ttcexg  37535  bj-ax6elem2  37781  ax6er  37960  bj-vtoclf  38042  wl-exeq  38734  exbiii  43528  cbvex2ivw  43529  sn-exelALT  43540  spd  51192  elpglem2  51211  eximp-surprise2  51309