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 1782

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

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

This theorem is referenced by:  exan  1866  ax6evr  2019  spimedv  2191  spimfv  2233  ax6e  2383  spim  2387  spimed  2388  spimvALT  2391  spei  2394  equvini  2455  equvel  2456  euequ  2592  dariiALT  2662  barbariALT  2666  festinoALT  2671  barocoALT  2673  daraptiALT  2681  vtoclfOLD  3547  axrep2  5284  axnul  5301  nalset  5309  notzfaus  5357  elALT2  5363  dtruALT2  5364  dvdemo1  5367  dvdemo2  5368  eusv2nf  5389  axprALT  5416  axpr  5422  exel  5429  dtruOLD  5437  inf1  9604  bnd  9874  axpowndlem2  10580  grothomex  10811  tgjustc1  27693  tgjustc2  27694  bnj101  33665  axextdfeq  34700  ax8dfeq  34701  axextndbi  34707  snelsingles  34825  bj-ax6elem2  35449  ax6er  35616  bj-vtoclf  35700  wl-exeq  36308  sn-exelALT  40951  spd  47563  elpglem2  47597  eximp-surprise2  47672