Theorem eximii 1857

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

Syntax hints:   → wi 4  ∃wex 1799

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

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

This theorem is referenced by:  exan  1882  ax6evr  2035  spimedv  2232  spimfv  2274  ax6e  2414  spim  2418  spimed  2419  spimvALT  2422  spei  2425  equvini  2486  equvel  2487  euequ  2624  dariiALT  2692  barbariALT  2696  festinoALT  2701  barocoALT  2703  daraptiALT  2711  ceqsexv2d  3503  axrep2  5230  axnul  5255  exnelv  5263  nalsetOLD  5265  notzfaus  5320  axpow3  5325  elALT2  5326  dtruALT2  5327  dvdemo1  5330  dvdemo2  5331  eusv2nf  5352  axprALT  5379  axprlem1  5380  axprOLD  5389  exel  5401  el  5405  elirrvOLD  9546  inf1  9577  omex  9598  bnd  9850  axpowndlem2  10556  grothomex  10787  tgjustc1  28644  tgjustc2  28645  bnj101  35019  axnulALT3  35404  axprALT2  35405  axsepg2  35436  axsepg3  35437  axsepg3ALT  35438  axsepg4  35439  axpowg2  35443  axpowg3  35444  axextdfeq  36145  ax8dfeq  36146  axextndbi  36152  snelsingles  36270  axtco  36831  axtco2  36834  axuntco  36839  elALTtco  36841  tz9.1tco  36843  ttcexg  36892  bj-ax6elem2  37139  ax6er  37318  bj-vtoclf  37400  wl-exeq  38037  exbiii  42827  sn-exelALT  42838  spd  50299  elpglem2  50333  eximp-surprise2  50406