Theorem eximii 1864

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

Syntax hints:   → wi 4  ∃wex 1806

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

This theorem depends on definitions:  df-bi 210  df-ex 1807

This theorem is referenced by:  exan  1889  ax6evr  2042  spimedv  2239  spimfv  2281  ax6e  2421  spim  2425  spimed  2426  spimvALT  2429  spei  2432  equvini  2493  equvel  2494  euequ  2631  dariiALT  2699  barbariALT  2703  festinoALT  2708  barocoALT  2710  daraptiALT  2718  ceqsexv2d  3512  axrep2  5245  axnul  5270  exnelv  5278  nalsetOLD  5280  notzfaus  5335  axpow3  5340  elALT2  5341  dtruALT2  5342  dvdemo1  5345  dvdemo2  5346  eusv2nf  5367  axprALT  5394  axprlem1  5395  axprOLD  5404  exel  5416  el  5420  elirrvOLD  9559  inf1  9590  omex  9611  bnd  9877  axpowndlem2  10582  grothomex  10813  tgjustc1  28709  tgjustc2  28710  bnj101  35056  axnulALT3  35443  axprALT2  35444  axsepg2  35475  axsepg3  35476  axsepg3ALT  35477  axsepg4  35478  axpowg2  35482  axpowg3  35483  axextdfeq  36185  ax8dfeq  36186  axextndbi  36192  snelsingles  36310  axtco  36870  axtco2  36873  axuntco  36878  elALTtco  36880  tz9.1tco  36882  ttcexg  36931  bj-ax6elem2  37177  ax6er  37356  bj-vtoclf  37438  wl-exeq  38076  exbiii  42868  sn-exelALT  42879  spd  50340  elpglem2  50374  eximp-surprise2  50447