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 206  df-ex 1782

This theorem is referenced by:  exan  1865  ax6evr  2018  spimedv  2190  spimfv  2232  ax6e  2382  spim  2386  spimed  2387  spimvALT  2390  spei  2393  equvini  2454  equvel  2455  euequ  2591  dariiALT  2661  barbariALT  2665  festinoALT  2670  barocoALT  2672  daraptiALT  2680  vtoclfOLD  3548  axrep2  5288  axnul  5305  nalset  5313  notzfaus  5361  elALT2  5367  dtruALT2  5368  dvdemo1  5371  dvdemo2  5372  eusv2nf  5393  axprALT  5420  axpr  5426  exel  5433  dtruOLD  5441  inf1  9616  bnd  9886  axpowndlem2  10592  grothomex  10823  tgjustc1  27723  tgjustc2  27724  bnj101  33729  axextdfeq  34764  ax8dfeq  34765  axextndbi  34771  snelsingles  34889  bj-ax6elem2  35539  ax6er  35706  bj-vtoclf  35790  wl-exeq  36398  sn-exelALT  41037  spd  47713  elpglem2  47747  eximp-surprise2  47822