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  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  5235  axnul  5262  exnelv  5270  nalsetOLD  5272  notsep  5328  axpow3  5333  elALT2  5334  dtruALT2  5335  dvdemo1  5338  dvdemo2  5339  eusv2nf  5360  axprALT  5387  axprlem1  5388  axprOLD  5397  exel  5409  el  5413  uniex2  7739  elirrvOLD  9570  inf1  9601  omex  9622  bnd  9894  axpowndlem2  10607  grothomex  10838  tgjustc1  28816  tgjustc2  28817  bnj101  35233  axnulALT3  35616  axprALT2  35617  axsepg2  35666  axsepg3  35667  axsepg3ALT  35668  axsepg4  35669  axpowg2  35673  axpowg3  35674  axextdfeq  36374  ax8dfeq  36375  axextndbi  36381  snelsingles  36499  axtco  37090  axtco2  37093  axuntco  37098  elALTtco  37100  tz9.1tco  37102  ttcexg  37151  bj-ax6elem2  37397  ax6er  37576  bj-vtoclf  37658  wl-exeq  38297  exbiii  43078  sn-exelALT  43089  spd  50604  elpglem2  50638  eximp-surprise2  50714