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  2048  spimedv  2236  spimfv  2278  ax6e  2417  spim  2421  spimed  2422  spimvALT  2425  spei  2428  equvini  2489  equvel  2490  euequ  2627  dariiALT  2695  barbariALT  2699  festinoALT  2704  barocoALT  2706  daraptiALT  2714  ceqsexv2d  3506  axrep2  5243  axnul  5270  exnelv  5278  nalsetOLD  5280  notsep  5336  axpow3  5341  elALT2  5342  dtruALT2  5343  dvdemo1  5346  dvdemo2  5347  eusv2nf  5368  axprALT  5395  axprlem1  5396  axprOLD  5405  exel  5417  el  5421  uniex2  7745  elirrvOLD  9567  inf1  9598  omex  9619  bnd  9891  axpowndlem2  10598  grothomex  10829  tgjustc1  28795  tgjustc2  28796  bnj101  35177  axnulALT3  35560  axprALT2  35561  axsepg2  35610  axsepg3  35611  axsepg3ALT  35612  axsepg4  35613  axpowg2  35617  axpowg3  35618  axextdfeq  36324  ax8dfeq  36325  axextndbi  36331  snelsingles  36449  axtco  37039  axtco2  37042  axuntco  37047  elALTtco  37049  tz9.1tco  37051  ttcexg  37100  bj-ax6elem2  37346  ax6er  37525  bj-vtoclf  37607  wl-exeq  38246  exbiii  43037  sn-exelALT  43048  spd  50513  elpglem2  50547  eximp-surprise2  50620