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  3549  axrep2  5289  axnul  5306  nalset  5314  notzfaus  5362  elALT2  5368  dtruALT2  5369  dvdemo1  5372  dvdemo2  5373  eusv2nf  5394  axprALT  5421  axpr  5427  exel  5434  dtruOLD  5442  inf1  9617  bnd  9887  axpowndlem2  10593  grothomex  10824  tgjustc1  27726  tgjustc2  27727  bnj101  33734  axextdfeq  34769  ax8dfeq  34770  axextndbi  34776  snelsingles  34894  bj-ax6elem2  35544  ax6er  35711  bj-vtoclf  35795  wl-exeq  36403  sn-exelALT  41035  spd  47723  elpglem2  47757  eximp-surprise2  47832