Theorem eximii 1740

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

Syntax hints:   → wi 4  ∃wex 1692

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

This theorem depends on definitions:  df-bi 192  df-ex 1693

This theorem is referenced by:  exiftru  1839  spimeh  1873  equidOLD  1888  ax6evr  1891  spimv1  2110  cbv3hvOLD  2114  cbv3hvOLDOLD  2115  ax6e  2141  spim  2145  spimed  2146  spimv  2148  spei  2152  equvini  2229  equvel  2230  euequ1  2359  euex  2377  darii  2448  barbari  2450  festino  2454  baroco  2455  cesaro  2456  camestros  2457  datisi  2458  disamis  2459  felapton  2462  darapti  2463  dimatis  2465  fresison  2466  calemos  2467  fesapo  2468  bamalip  2469  vtoclf  3120  vtocl  3121  axrep2  4550  axnul  4565  nalset  4573  notzfaus  4616  el  4623  dtru  4633  eusv2nf  4640  dvdemo1  4676  dvdemo2  4677  axpr  4679  snnex  6674  inf1  8212  bnd  8448  axpowndlem2  9108  grothomex  9339  bnj101  29682  axextdfeq  30595  ax8dfeq  30596  axextndbi  30602  snelsingles  30840  bj-ax6elem2  31447  bj-spimedv  31507  bj-spimvv  31509  bj-speiv  31512  bj-axrep2  31586  bj-nalset  31591  bj-el  31593  bj-dtru  31594  bj-dvdemo1  31599  bj-dvdemo2  31600  ax6er  31617  bj-vtoclf  31699  wl-exeq  32098  eximp-surprise2  41711