Theorem eximii 1761

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

Syntax hints:   → wi 4  ∃wex 1701

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

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

This theorem is referenced by:  exiftru  1893  spimeh  1927  ax6evr  1944  spimv1  2117  cbv3hvOLD  2177  cbv3hvOLDOLD  2178  ax6e  2254  spim  2258  spimed  2259  spimv  2261  spei  2265  equvini  2350  equvel  2351  euequ1  2480  euex  2498  darii  2569  barbari  2571  festino  2575  baroco  2576  cesaro  2577  camestros  2578  datisi  2579  disamis  2580  felapton  2583  darapti  2584  dimatis  2586  fresison  2587  calemos  2588  fesapo  2589  bamalip  2590  vtoclf  3249  vtocl  3250  axrep2  4738  axnul  4753  nalset  4760  notzfaus  4805  el  4812  dtru  4822  eusv2nf  4829  dvdemo1  4868  dvdemo2  4869  axpr  4871  snnex  6918  inf1  8464  bnd  8700  axpowndlem2  9365  grothomex  9596  bnj101  30489  axextdfeq  31392  ax8dfeq  31393  axextndbi  31399  snelsingles  31644  bj-ax6elem2  32267  bj-spimedv  32334  bj-spimvv  32336  bj-speiv  32339  bj-axrep2  32405  bj-nalset  32410  bj-el  32412  bj-dtru  32413  bj-dvdemo1  32418  bj-dvdemo2  32419  ax6er  32436  bj-vtoclf  32528  wl-exeq  32929  spd  41672  elpglem2  41703  eximp-surprise2  41789