Theorem eximii 1869

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  exan  1894  ax6evr  2047  spimedv  2233  spimfv  2275  ax6e  2412  spim  2416  spimed  2417  spimvALT  2420  spei  2423  equvini  2484  equvel  2485  euequ  2622  dariiALT  2690  barbariALT  2694  festinoALT  2699  barocoALT  2701  daraptiALT  2709  ceqsexv2d  3499  axrep2  5234  axnul  5258  exnelv  5266  nalsetOLD  5268  notsep  5325  axpow3  5330  elALT2  5331  dtruALT2  5332  dvdemo1  5335  dvdemo2  5336  eusv2nf  5357  axprALT  5384  axprlem1  5385  exel  5402  el  5406  uniex2  7758  elirrvOLD  9599  inf1  9630  omex  9651  bnd  9962  axpowndlem2  10690  grothomex  10921  tgjustc1  28946  tgjustc2  28947  bnj101  35404  axnulALT3  35789  axprALT2  35790  axsepg2  35868  axsepg3  35869  axsepg3ALT  35870  axsepg4  35871  axpowg2  35875  axpowg3  35876  axextdfeq  36655  ax8dfeq  36656  axextndbi  36662  snelsingles  36780  axtco  37355  axtco2  37358  axuntco  37363  elALTtco  37365  tz9.1tco  37367  ttcexg  37416  bj-ax6elem2  37662  ax6er  37841  bj-vtoclf  37923  wl-exeq  38575  exbiii  43371  sn-exelALT  43382  spd  50969  elpglem2  50988  eximp-surprise2  51064