Theorem eximii 1844

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

Syntax hints:   → wi 4  ∃wex 1786

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

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  exan  1869  ax6evr  2022  spimedv  2209  spimfv  2251  ax6e  2391  spim  2395  spimed  2396  spimvALT  2399  spei  2402  equvini  2463  equvel  2464  euequ  2601  dariiALT  2669  barbariALT  2673  festinoALT  2678  barocoALT  2680  daraptiALT  2688  ceqsexv2d  3480  axrep2  5202  axnul  5227  exnelv  5235  nalsetOLD  5237  notzfaus  5292  axpow3  5297  elALT2  5298  dtruALT2  5299  dvdemo1  5302  dvdemo2  5303  eusv2nf  5324  axprALT  5351  axprlem1  5352  axprOLD  5361  exel  5373  el  5377  elirrvOLD  9503  inf1  9534  omex  9555  bnd  9807  axpowndlem2  10512  grothomex  10743  tgjustc1  28561  tgjustc2  28562  bnj101  34906  axnulALT3  35289  axprALT2  35290  axsepg2  35321  axsepg3  35322  axsepg3ALT  35323  axsepg4  35324  axpowg2  35328  axpowg3  35329  axextdfeq  36023  ax8dfeq  36024  axextndbi  36030  snelsingles  36148  axtco  36699  axtco2  36702  axuntco  36707  elALTtco  36709  tz9.1tco  36711  ttcexg  36760  bj-ax6elem2  37007  ax6er  37186  bj-vtoclf  37268  wl-exeq  37905  exbiii  42695  sn-exelALT  42706  spd  50168  elpglem2  50202  eximp-surprise2  50275