Theorem eximii 1860

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

Syntax hints:   → wi 4  ∃wex 1802

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

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

This theorem is referenced by:  exan  1885  ax6evr  2038  spimedv  2235  spimfv  2277  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  5234  axnul  5259  exnelv  5267  nalsetOLD  5269  notzfaus  5324  axpow3  5329  elALT2  5330  dtruALT2  5331  dvdemo1  5334  dvdemo2  5335  eusv2nf  5356  axprALT  5383  axprlem1  5384  axprOLD  5393  exel  5405  el  5409  elirrvOLD  9548  inf1  9579  omex  9600  bnd  9866  axpowndlem2  10571  grothomex  10802  tgjustc1  28698  tgjustc2  28699  bnj101  35024  axnulALT3  35411  axprALT2  35412  axsepg2  35443  axsepg3  35444  axsepg3ALT  35445  axsepg4  35446  axpowg2  35450  axpowg3  35451  axextdfeq  36153  ax8dfeq  36154  axextndbi  36160  snelsingles  36278  axtco  36839  axtco2  36842  axuntco  36847  elALTtco  36849  tz9.1tco  36851  ttcexg  36900  bj-ax6elem2  37146  ax6er  37325  bj-vtoclf  37407  wl-exeq  38044  exbiii  42834  sn-exelALT  42845  spd  50308  elpglem2  50342  eximp-surprise2  50415