Theorem eximii 1838

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

Syntax hints:   → wi 4  ∃wex 1780

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

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

This theorem is referenced by:  exan  1863  ax6evr  2016  spimedv  2202  spimfv  2244  ax6e  2385  spim  2389  spimed  2390  spimvALT  2393  spei  2396  equvini  2457  equvel  2458  euequ  2594  dariiALT  2663  barbariALT  2667  festinoALT  2672  barocoALT  2674  daraptiALT  2682  ceqsexv2d  3489  axrep2  5224  axnul  5247  nalset  5255  notzfaus  5305  axpow3  5310  elALT2  5311  dtruALT2  5312  dvdemo1  5315  dvdemo2  5316  eusv2nf  5337  axprALT  5364  axprOLD  5373  exel  5380  elirrv  9493  inf1  9522  omex  9543  bnd  9795  axpowndlem2  10499  grothomex  10730  tgjustc1  28463  tgjustc2  28464  bnj101  34746  axsepg2  35105  axsepg2ALT  35106  axnulALT2  35131  axextdfeq  35850  ax8dfeq  35851  axextndbi  35857  snelsingles  35975  bj-ax6elem2  36722  ax6er  36888  bj-vtoclf  36970  wl-exeq  37589  exbiii  42313  sn-exelALT  42326  spd  49793  elpglem2  49827  eximp-surprise2  49900