Theorem eximii 1835

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

Syntax hints:   → wi 4  ∃wex 1777

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

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

This theorem is referenced by:  exan  1861  ax6evr  2014  spimedv  2198  spimfv  2240  ax6e  2391  spim  2395  spimed  2396  spimvALT  2399  spei  2402  equvini  2463  equvel  2464  euequ  2600  dariiALT  2669  barbariALT  2673  festinoALT  2678  barocoALT  2680  daraptiALT  2688  ceqsexv2d  3545  vtoclfOLD  3577  axrep2  5306  axnul  5323  nalset  5331  notzfaus  5381  elALT2  5387  dtruALT2  5388  dvdemo1  5391  dvdemo2  5392  eusv2nf  5413  axprALT  5440  axpr  5446  exel  5453  dtruOLD  5461  inf1  9691  bnd  9961  axpowndlem2  10667  grothomex  10898  tgjustc1  28501  tgjustc2  28502  bnj101  34699  axsepg2  35058  axsepg2ALT  35059  axnulALT2  35069  axextdfeq  35761  ax8dfeq  35762  axextndbi  35768  snelsingles  35886  bj-ax6elem2  36633  ax6er  36799  bj-vtoclf  36881  wl-exeq  37488  sn-exelALT  42211  spd  48770  elpglem2  48804  eximp-surprise2  48879