Theorem eximii 1843

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

Syntax hints:   → wi 4  ∃wex 1786

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

This theorem depends on definitions:  df-bi 210  df-ex 1787

This theorem is referenced by:  exan  1868  spimehOLD  1979  exgenOLD  1983  ax6evr  2026  spimedv  2198  spimfv  2240  ax6e  2382  spim  2386  spimed  2387  spimvALT  2390  spei  2393  equvini  2454  equvel  2455  euequ  2598  dariiALT  2668  barbariALT  2672  festinoALT  2677  barocoALT  2679  daraptiALT  2687  vtoclf  3462  axrep2  5154  axnul  5170  nalset  5178  notzfaus  5225  notzfausOLD  5226  el  5233  dtru  5234  dvdemo1  5237  dvdemo2  5238  eusv2nf  5259  axprALT  5286  axpr  5292  inf1  9151  bnd  9387  axpowndlem2  10091  grothomex  10322  tgjustc1  26413  tgjustc2  26414  bnj101  32264  axextdfeq  33337  ax8dfeq  33338  axextndbi  33344  snelsingles  33854  bj-ax6elem2  34475  bj-dtru  34619  ax6er  34636  bj-vtoclf  34721  wl-exeq  35305  sn-el  39762  spd  45821  elpglem2  45854  eximp-surprise2  45926