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  3499  vtoclfOLD  3531  axrep2  5237  axnul  5260  nalset  5268  notzfaus  5318  axpow3  5323  elALT2  5324  dtruALT2  5325  dvdemo1  5328  dvdemo2  5329  eusv2nf  5350  axprALT  5377  axprOLD  5386  exel  5393  dtruOLD  5401  inf1  9575  omex  9596  bnd  9845  axpowndlem2  10551  grothomex  10782  tgjustc1  28402  tgjustc2  28403  bnj101  34713  axsepg2  35072  axsepg2ALT  35073  axnulALT2  35083  axextdfeq  35785  ax8dfeq  35786  axextndbi  35792  snelsingles  35910  bj-ax6elem2  36655  ax6er  36821  bj-vtoclf  36903  wl-exeq  37522  exbiii  42198  sn-exelALT  42206  spd  49667  elpglem2  49701  eximp-surprise2  49774