Theorem eximii 1837

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

Syntax hints:   → wi 4  ∃wex 1780

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

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

This theorem is referenced by:  exan  1862  exanOLD  1863  spimehOLD  1975  exgenOLD  1979  ax6evr  2022  spimedv  2197  spimfv  2241  ax6e  2401  spim  2405  spimed  2406  spimvALT  2409  spei  2412  equvini  2477  equviniOLD  2478  equvel  2479  equsb1vOLDOLD  2517  euequ  2683  dariiALT  2751  barbariALT  2755  festinoALT  2760  barocoALT  2762  daraptiALT  2770  vtoclf  3560  axrep2  5195  axnul  5211  nalset  5219  notzfaus  5264  notzfausOLD  5265  el  5272  dtru  5273  dvdemo1  5276  dvdemo2  5277  eusv2nf  5298  axprALT  5325  axpr  5331  inf1  9087  bnd  9323  axpowndlem2  10022  grothomex  10253  tgjustc1  26263  tgjustc2  26264  bnj101  31995  axextdfeq  33044  ax8dfeq  33045  axextndbi  33051  snelsingles  33385  bj-ax6elem2  34002  bj-dtru  34141  ax6er  34158  bj-vtoclf  34233  wl-exeq  34776  sn-el  39117  spd  44788  elpglem2  44821  eximp-surprise2  44893