Theorem eximii 1840

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

Syntax hints:   → wi 4  ∃wex 1782

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

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  exan  1866  ax6evr  2019  spimedv  2191  spimfv  2233  ax6e  2383  spim  2387  spimed  2388  spimvALT  2391  spei  2394  equvini  2455  equvel  2456  euequ  2592  dariiALT  2662  barbariALT  2666  festinoALT  2671  barocoALT  2673  daraptiALT  2681  vtoclfOLD  3549  axrep2  5289  axnul  5306  nalset  5314  notzfaus  5362  elALT2  5368  dtruALT2  5369  dvdemo1  5372  dvdemo2  5373  eusv2nf  5394  axprALT  5421  axpr  5427  exel  5434  dtruOLD  5442  inf1  9617  bnd  9887  axpowndlem2  10593  grothomex  10824  tgjustc1  27757  tgjustc2  27758  bnj101  33765  axextdfeq  34800  ax8dfeq  34801  axextndbi  34807  snelsingles  34925  bj-ax6elem2  35592  ax6er  35759  bj-vtoclf  35843  wl-exeq  36451  sn-exelALT  41083  spd  47771  elpglem2  47805  eximp-surprise2  47880