Theorem eximii 1833

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

Syntax hints:   → wi 4  ∃wex 1776

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

This theorem depends on definitions:  df-bi 209  df-ex 1777

This theorem is referenced by:  exan  1858  exanOLD  1859  spimehOLD  1971  exgenOLD  1975  ax6evr  2018  spimedv  2192  spimfv  2236  ax6e  2397  spim  2401  spimed  2402  spimvALT  2405  spei  2408  equvini  2473  equviniOLD  2474  equvel  2475  equsb1vOLDOLD  2513  euequ  2679  dariiALT  2749  barbariALT  2753  festinoALT  2758  barocoALT  2760  daraptiALT  2768  vtoclf  3559  vtocl  3560  axrep2  5186  axnul  5202  nalset  5210  notzfaus  5255  notzfausOLD  5256  el  5263  dtru  5264  dvdemo1  5267  dvdemo2  5268  eusv2nf  5288  axprALT  5315  axpr  5321  inf1  9079  bnd  9315  axpowndlem2  10014  grothomex  10245  tgjustc1  26255  tgjustc2  26256  bnj101  31988  axextdfeq  33037  ax8dfeq  33038  axextndbi  33044  snelsingles  33378  bj-ax6elem2  33995  bj-dtru  34134  ax6er  34151  bj-vtoclf  34226  wl-exeq  34768  sn-el  39103  spd  44774  elpglem2  44807  eximp-surprise2  44879