Theorem eximii 1839

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

Syntax hints:   → wi 4  ∃wex 1781

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

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  exan  1864  ax6evr  2017  spimedv  2205  spimfv  2247  ax6e  2387  spim  2391  spimed  2392  spimvALT  2395  spei  2398  equvini  2459  equvel  2460  euequ  2597  dariiALT  2666  barbariALT  2670  festinoALT  2675  barocoALT  2677  daraptiALT  2685  ceqsexv2d  3479  axrep2  5215  axnul  5240  exnelv  5248  nalsetOLD  5250  notzfaus  5305  axpow3  5310  elALT2  5311  dtruALT2  5312  dvdemo1  5315  dvdemo2  5316  eusv2nf  5337  axprALT  5364  axprlem1  5365  axprOLD  5374  exel  5386  el  5390  elirrv  9512  inf1  9543  omex  9564  bnd  9816  axpowndlem2  10521  grothomex  10752  tgjustc1  28543  tgjustc2  28544  bnj101  34866  axsepg2  35225  axsepg2ALT  35226  axnulALT3  35252  axprALT2  35253  axextdfeq  35977  ax8dfeq  35978  axextndbi  35984  snelsingles  36102  axtco  36653  axtco2  36656  axuntco  36661  elALTtco  36663  tz9.1tco  36665  ttcexg  36714  bj-ax6elem2  36961  ax6er  37140  bj-vtoclf  37222  wl-exeq  37859  exbiii  42649  sn-exelALT  42660  spd  50153  elpglem2  50187  eximp-surprise2  50260