Theorem eximii 1937

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

Syntax hints:   → wi 4  ∃wex 1880

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

This theorem depends on definitions:  df-bi 199  df-ex 1881

This theorem is referenced by:  exgen  2080  spimeh  2103  ax6evr  2121  spimv1  2298  ax6e  2404  spim  2409  spimed  2410  spimvALT  2413  spei  2416  equvini  2477  equvel  2478  euequ  2670  euequOLD  2671  euexOLD  2683  dariiALT  2750  barbariALT  2754  festinoALT  2761  barocoALT  2763  cesaroOLD  2765  camestrosOLD  2767  datisiOLD  2769  disamisOLD  2771  daraptiALT  2775  dimatisOLD  2780  fresisonOLD  2782  calemosOLD  2784  fesapoOLD  2786  bamalipOLD  2788  vtoclf  3475  vtocl  3476  axrep2  4998  axnul  5013  nalset  5021  notzfaus  5063  el  5070  dtru  5071  dvdemo1  5074  dvdemo2  5075  eusv2nf  5096  axpr  5127  inf1  8797  bnd  9033  axpowndlem2  9736  grothomex  9967  tgjustc1  25788  tgjustc2  25789  bnj101  31339  axextdfeq  32242  ax8dfeq  32243  axextndbi  32249  snelsingles  32569  bj-ax6elem2  33189  bj-spimedv  33254  bj-spimvv  33256  bj-speiv  33259  bj-axrep2  33315  bj-nalset  33320  bj-el  33322  bj-dtru  33323  bj-dvdemo1  33328  bj-dvdemo2  33329  ax6er  33345  bj-vtoclf  33431  wl-exeq  33866  spd  43321  elpglem2  43354  eximp-surprise2  43428