Theorem eximii 1840

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

Syntax hints:   → wi 4  ∃wex 1783

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

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  exan  1866  ax6evr  2019  spimedv  2193  spimfv  2235  ax6e  2383  spim  2387  spimed  2388  spimvALT  2391  spei  2394  equvini  2455  equvel  2456  euequ  2597  dariiALT  2667  barbariALT  2671  festinoALT  2676  barocoALT  2678  daraptiALT  2686  vtoclf  3487  axrep2  5208  axnul  5224  nalset  5232  notzfaus  5280  el  5287  dtru  5288  dvdemo1  5291  dvdemo2  5292  eusv2nf  5313  axprALT  5340  axpr  5346  inf1  9310  bnd  9581  axpowndlem2  10285  grothomex  10516  tgjustc1  26740  tgjustc2  26741  bnj101  32602  axextdfeq  33679  ax8dfeq  33680  axextndbi  33686  snelsingles  34151  bj-ax6elem2  34775  bj-dtru  34926  ax6er  34943  bj-vtoclf  35027  wl-exeq  35620  sn-el  40115  spd  46270  elpglem2  46303  eximp-surprise2  46375