Theorem eximii 1837

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

Syntax hints:   → wi 4  ∃wex 1779

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

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

This theorem is referenced by:  exan  1862  ax6evr  2015  spimedv  2198  spimfv  2240  ax6e  2381  spim  2385  spimed  2386  spimvALT  2389  spei  2392  equvini  2453  equvel  2454  euequ  2590  dariiALT  2659  barbariALT  2663  festinoALT  2668  barocoALT  2670  daraptiALT  2678  ceqsexv2d  3488  vtoclfOLD  3520  axrep2  5221  axnul  5244  nalset  5252  notzfaus  5302  axpow3  5307  elALT2  5308  dtruALT2  5309  dvdemo1  5312  dvdemo2  5313  eusv2nf  5334  axprALT  5361  axprOLD  5370  exel  5377  elirrv  9489  inf1  9518  omex  9539  bnd  9788  axpowndlem2  10492  grothomex  10723  tgjustc1  28420  tgjustc2  28421  bnj101  34690  axsepg2  35049  axsepg2ALT  35050  axnulALT2  35060  axextdfeq  35771  ax8dfeq  35772  axextndbi  35778  snelsingles  35896  bj-ax6elem2  36641  ax6er  36807  bj-vtoclf  36889  wl-exeq  37508  exbiii  42183  sn-exelALT  42191  spd  49663  elpglem2  49697  eximp-surprise2  49770