Theorem eximii 1839

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

Syntax hints:   → wi 4  ∃wex 1781

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

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

This theorem is referenced by:  exan  1864  ax6evr  2017  spimedv  2205  spimfv  2247  ax6e  2388  spim  2392  spimed  2393  spimvALT  2396  spei  2399  equvini  2460  equvel  2461  euequ  2598  dariiALT  2667  barbariALT  2671  festinoALT  2676  barocoALT  2678  daraptiALT  2686  ceqsexv2d  3493  axrep2  5229  axnul  5252  nalset  5260  notzfaus  5310  axpow3  5315  elALT2  5316  dtruALT2  5317  dvdemo1  5320  dvdemo2  5321  eusv2nf  5342  axprALT  5369  axprOLD  5378  exel  5390  elirrv  9514  inf1  9543  omex  9564  bnd  9816  axpowndlem2  10521  grothomex  10752  tgjustc1  28559  tgjustc2  28560  bnj101  34900  axsepg2  35259  axsepg2ALT  35260  axnulALT3  35286  axprALT2  35287  axextdfeq  36011  ax8dfeq  36012  axextndbi  36018  snelsingles  36136  bj-ax6elem2  36912  ax6er  37081  bj-vtoclf  37163  wl-exeq  37789  exbiii  42580  sn-exelALT  42591  spd  50037  elpglem2  50071  eximp-surprise2  50144