Theorem eximii 1834

Description: Inference associated with eximi 1832. (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 1832	. 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 207  df-ex 1777

This theorem is referenced by:  exan  1860  ax6evr  2012  spimedv  2195  spimfv  2237  ax6e  2386  spim  2390  spimed  2391  spimvALT  2394  spei  2397  equvini  2458  equvel  2459  euequ  2595  dariiALT  2664  barbariALT  2668  festinoALT  2673  barocoALT  2675  daraptiALT  2683  ceqsexv2d  3533  vtoclfOLD  3565  axrep2  5288  axnul  5311  nalset  5319  notzfaus  5369  elALT2  5375  dtruALT2  5376  dvdemo1  5379  dvdemo2  5380  eusv2nf  5401  axprALT  5428  axprOLD  5437  exel  5444  dtruOLD  5452  inf1  9660  bnd  9930  axpowndlem2  10636  grothomex  10867  tgjustc1  28498  tgjustc2  28499  bnj101  34716  axsepg2  35075  axsepg2ALT  35076  axnulALT2  35086  axextdfeq  35779  ax8dfeq  35780  axextndbi  35786  snelsingles  35904  bj-ax6elem2  36650  ax6er  36816  bj-vtoclf  36898  wl-exeq  37515  sn-exelALT  42236  spd  48909  elpglem2  48943  eximp-surprise2  49016