Theorem eximii 1867

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

Syntax hints:   → wi 4  ∃wex 1809

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

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

This theorem is referenced by:  exan  1892  ax6evr  2045  spimedv  2233  spimfv  2275  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  3504  axrep2  5241  axnul  5268  exnelv  5276  nalsetOLD  5278  notsep  5334  axpow3  5339  elALT2  5340  dtruALT2  5341  dvdemo1  5344  dvdemo2  5345  eusv2nf  5366  axprALT  5393  axprlem1  5394  axprOLD  5403  exel  5415  el  5419  uniex2  7735  elirrvOLD  9556  inf1  9587  omex  9608  bnd  9874  axpowndlem2  10578  grothomex  10809  tgjustc1  28744  tgjustc2  28745  bnj101  35112  axnulALT3  35502  axprALT2  35503  axsepg2  35553  axsepg3  35554  axsepg3ALT  35555  axsepg4  35556  axpowg2  35560  axpowg3  35561  axextdfeq  36287  ax8dfeq  36288  axextndbi  36294  snelsingles  36412  axtco  36982  axtco2  36985  axuntco  36990  elALTtco  36992  tz9.1tco  36994  ttcexg  37043  bj-ax6elem2  37289  ax6er  37468  bj-vtoclf  37550  wl-exeq  38189  exbiii  42979  sn-exelALT  42990  spd  50456  elpglem2  50490  eximp-surprise2  50563