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  2234  spimfv  2276  ax6e  2413  spim  2417  spimed  2418  spimvALT  2421  spei  2424  equvini  2485  equvel  2486  euequ  2623  dariiALT  2691  barbariALT  2695  festinoALT  2700  barocoALT  2702  daraptiALT  2710  ceqsexv2d  3500  axrep2  5235  axnul  5259  exnelv  5267  nalsetOLD  5269  notsep  5325  axpow3  5330  elALT2  5331  dtruALT2  5332  dvdemo1  5335  dvdemo2  5336  eusv2nf  5357  axprALT  5384  axprlem1  5385  exel  5402  el  5406  uniex2  7752  elirrvOLD  9585  inf1  9616  omex  9637  bnd  9948  axpowndlem2  10676  grothomex  10907  tgjustc1  28930  tgjustc2  28931  bnj101  35347  axnulALT3  35722  axprALT2  35723  axsepg2  35791  axsepg3  35792  axsepg3ALT  35793  axsepg4  35794  axpowg2  35798  axpowg3  35799  axextdfeq  36539  ax8dfeq  36540  axextndbi  36546  snelsingles  36664  axtco  37239  axtco2  37242  axuntco  37247  elALTtco  37249  tz9.1tco  37251  ttcexg  37300  bj-ax6elem2  37546  ax6er  37725  bj-vtoclf  37807  wl-exeq  38446  exbiii  43242  sn-exelALT  43253  spd  50755  elpglem2  50774  eximp-surprise2  50850