Theorem eximii 1804

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

Syntax hints:   → wi 4  ∃wex 1744

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

This theorem depends on definitions:  df-bi 197  df-ex 1745

This theorem is referenced by:  exiftru  1948  spimeh  1971  ax6evr  1988  spimv1  2153  ax6e  2286  spim  2290  spimed  2291  spimv  2293  spei  2297  equvini  2374  equvel  2375  euequ1  2504  euex  2522  darii  2594  barbari  2596  festino  2600  baroco  2601  cesaro  2602  camestros  2603  datisi  2604  disamis  2605  felapton  2608  darapti  2609  dimatis  2611  fresison  2612  calemos  2613  fesapo  2614  bamalip  2615  vtoclf  3289  vtocl  3290  axrep2  4806  axnul  4821  nalset  4828  notzfaus  4870  el  4877  dtru  4887  eusv2nf  4894  dvdemo1  4932  dvdemo2  4933  axpr  4935  snnexOLD  7009  inf1  8557  bnd  8793  axpowndlem2  9458  grothomex  9689  bnj101  30917  axextdfeq  31827  ax8dfeq  31828  axextndbi  31834  snelsingles  32154  bj-ax6elem2  32777  bj-spimedv  32844  bj-spimvv  32846  bj-speiv  32849  bj-axrep2  32914  bj-nalset  32919  bj-el  32921  bj-dtru  32922  bj-dvdemo1  32927  bj-dvdemo2  32928  ax6er  32945  bj-vtoclf  33033  wl-exeq  33451  spd  42750  elpglem2  42783  eximp-surprise2  42859