Theorem eximii 1836

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

Syntax hints:   → wi 4  ∃wex 1778

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

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

This theorem is referenced by:  exan  1861  ax6evr  2013  spimedv  2196  spimfv  2238  ax6e  2387  spim  2391  spimed  2392  spimvALT  2395  spei  2398  equvini  2459  equvel  2460  euequ  2596  dariiALT  2665  barbariALT  2669  festinoALT  2674  barocoALT  2676  daraptiALT  2684  ceqsexv2d  3532  vtoclfOLD  3564  axrep2  5281  axnul  5304  nalset  5312  notzfaus  5362  axpow3  5367  elALT2  5368  dtruALT2  5369  dvdemo1  5372  dvdemo2  5373  eusv2nf  5394  axprALT  5421  axprOLD  5430  exel  5437  dtruOLD  5445  inf1  9663  omex  9684  bnd  9933  axpowndlem2  10639  grothomex  10870  tgjustc1  28484  tgjustc2  28485  bnj101  34738  axsepg2  35097  axsepg2ALT  35098  axnulALT2  35108  axextdfeq  35799  ax8dfeq  35800  axextndbi  35806  snelsingles  35924  bj-ax6elem2  36669  ax6er  36835  bj-vtoclf  36917  wl-exeq  37536  exbiii  42250  sn-exelALT  42258  spd  49252  elpglem2  49286  eximp-surprise2  49359