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  2202  spimfv  2244  ax6e  2385  spim  2389  spimed  2390  spimvALT  2393  spei  2396  equvini  2457  equvel  2458  euequ  2595  dariiALT  2664  barbariALT  2668  festinoALT  2673  barocoALT  2675  daraptiALT  2683  ceqsexv2d  3489  axrep2  5225  axnul  5248  nalset  5256  notzfaus  5306  axpow3  5311  elALT2  5312  dtruALT2  5313  dvdemo1  5316  dvdemo2  5317  eusv2nf  5338  axprALT  5365  axprOLD  5374  exel  5381  elirrv  9500  inf1  9529  omex  9550  bnd  9802  axpowndlem2  10507  grothomex  10738  tgjustc1  28496  tgjustc2  28497  bnj101  34828  axsepg2  35187  axsepg2ALT  35188  axnulALT2  35214  axextdfeq  35938  ax8dfeq  35939  axextndbi  35945  snelsingles  36063  bj-ax6elem2  36811  ax6er  36977  bj-vtoclf  37059  wl-exeq  37678  exbiii  42403  sn-exelALT  42416  spd  49865  elpglem2  49899  eximp-surprise2  49972