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  2200  spimfv  2242  ax6e  2383  spim  2387  spimed  2388  spimvALT  2391  spei  2394  equvini  2455  equvel  2456  euequ  2592  dariiALT  2661  barbariALT  2665  festinoALT  2670  barocoALT  2672  daraptiALT  2680  ceqsexv2d  3487  axrep2  5218  axnul  5241  nalset  5249  notzfaus  5299  axpow3  5304  elALT2  5305  dtruALT2  5306  dvdemo1  5309  dvdemo2  5310  eusv2nf  5331  axprALT  5358  axprOLD  5367  exel  5374  elirrv  9483  inf1  9512  omex  9533  bnd  9785  axpowndlem2  10489  grothomex  10720  tgjustc1  28453  tgjustc2  28454  bnj101  34735  axsepg2  35094  axsepg2ALT  35095  axnulALT2  35120  axextdfeq  35839  ax8dfeq  35840  axextndbi  35846  snelsingles  35964  bj-ax6elem2  36709  ax6er  36875  bj-vtoclf  36957  wl-exeq  37576  exbiii  42251  sn-exelALT  42259  spd  49718  elpglem2  49752  eximp-surprise2  49825