Theorem eximii 1839

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

Syntax hints:   → wi 4  ∃wex 1781

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

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  exan  1864  ax6evr  2017  spimedv  2205  spimfv  2247  ax6e  2388  spim  2392  spimed  2393  spimvALT  2396  spei  2399  equvini  2460  equvel  2461  euequ  2598  dariiALT  2667  barbariALT  2671  festinoALT  2676  barocoALT  2678  daraptiALT  2686  ceqsexv2d  3480  axrep2  5216  axnul  5241  exnelv  5249  nalsetOLD  5251  notzfaus  5301  axpow3  5306  elALT2  5307  dtruALT2  5308  dvdemo1  5311  dvdemo2  5312  eusv2nf  5333  axprALT  5360  axprlem1  5361  axprOLD  5370  exel  5382  el  5386  elirrv  9506  inf1  9537  omex  9558  bnd  9810  axpowndlem2  10515  grothomex  10746  tgjustc1  28560  tgjustc2  28561  bnj101  34885  axsepg2  35244  axsepg2ALT  35245  axnulALT3  35271  axprALT2  35272  axextdfeq  35996  ax8dfeq  35997  axextndbi  36003  snelsingles  36121  axtco  36672  axtco2  36675  axuntco  36680  elALTtco  36682  tz9.1tco  36684  ttcexg  36733  bj-ax6elem2  36980  ax6er  37159  bj-vtoclf  37241  wl-exeq  37876  exbiii  42666  sn-exelALT  42677  spd  50168  elpglem2  50202  eximp-surprise2  50275