Theorem eximii 1754

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

Syntax hints:   → wi 4  ∃wex 1695

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

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  exiftru  1878  spimeh  1912  ax6evr  1929  spimv1  2101  cbv3hvOLD  2161  cbv3hvOLDOLD  2162  ax6e  2238  spim  2242  spimed  2243  spimv  2245  spei  2249  equvini  2334  equvel  2335  euequ1  2464  euex  2482  darii  2553  barbari  2555  festino  2559  baroco  2560  cesaro  2561  camestros  2562  datisi  2563  disamis  2564  felapton  2567  darapti  2568  dimatis  2570  fresison  2571  calemos  2572  fesapo  2573  bamalip  2574  vtoclf  3231  vtocl  3232  axrep2  4701  axnul  4716  nalset  4723  notzfaus  4766  el  4773  dtru  4783  eusv2nf  4790  dvdemo1  4829  dvdemo2  4830  axpr  4832  snnex  6862  inf1  8402  bnd  8638  axpowndlem2  9299  grothomex  9530  bnj101  30043  axextdfeq  30947  ax8dfeq  30948  axextndbi  30954  snelsingles  31199  bj-ax6elem2  31841  bj-spimedv  31906  bj-spimvv  31908  bj-speiv  31911  bj-axrep2  31977  bj-nalset  31982  bj-el  31984  bj-dtru  31985  bj-dvdemo1  31990  bj-dvdemo2  31991  ax6er  32008  bj-vtoclf  32100  wl-exeq  32500  spd  42223  elpglem2  42254  eximp-surprise2  42340