Theorem eximii 1838

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

Syntax hints:   → wi 4  ∃wex 1780

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

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

This theorem is referenced by:  exan  1863  ax6evr  2016  spimedv  2204  spimfv  2246  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  3491  axrep2  5227  axnul  5250  nalset  5258  notzfaus  5308  axpow3  5313  elALT2  5314  dtruALT2  5315  dvdemo1  5318  dvdemo2  5319  eusv2nf  5340  axprALT  5367  axprOLD  5376  exel  5383  elirrv  9502  inf1  9531  omex  9552  bnd  9804  axpowndlem2  10509  grothomex  10740  tgjustc1  28547  tgjustc2  28548  bnj101  34879  axsepg2  35238  axsepg2ALT  35239  axnulALT2  35265  axextdfeq  35989  ax8dfeq  35990  axextndbi  35996  snelsingles  36114  bj-ax6elem2  36868  ax6er  37034  bj-vtoclf  37116  wl-exeq  37739  exbiii  42464  sn-exelALT  42475  spd  49923  elpglem2  49957  eximp-surprise2  50030