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 1779

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

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

This theorem is referenced by:  exan  1862  ax6evr  2015  spimedv  2198  spimfv  2240  ax6e  2388  spim  2392  spimed  2393  spimvALT  2396  spei  2399  equvini  2460  equvel  2461  euequ  2597  dariiALT  2666  barbariALT  2670  festinoALT  2675  barocoALT  2677  daraptiALT  2685  ceqsexv2d  3517  vtoclfOLD  3549  axrep2  5257  axnul  5280  nalset  5288  notzfaus  5338  axpow3  5343  elALT2  5344  dtruALT2  5345  dvdemo1  5348  dvdemo2  5349  eusv2nf  5370  axprALT  5397  axprOLD  5406  exel  5413  dtruOLD  5421  inf1  9641  omex  9662  bnd  9911  axpowndlem2  10617  grothomex  10848  tgjustc1  28459  tgjustc2  28460  bnj101  34759  axsepg2  35118  axsepg2ALT  35119  axnulALT2  35129  axextdfeq  35820  ax8dfeq  35821  axextndbi  35827  snelsingles  35945  bj-ax6elem2  36690  ax6er  36856  bj-vtoclf  36938  wl-exeq  37557  exbiii  42228  sn-exelALT  42236  spd  49522  elpglem2  49556  eximp-surprise2  49629