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  2381  spim  2385  spimed  2386  spimvALT  2389  spei  2392  equvini  2453  equvel  2454  euequ  2590  dariiALT  2659  barbariALT  2663  festinoALT  2668  barocoALT  2670  daraptiALT  2678  ceqsexv2d  3496  vtoclfOLD  3528  axrep2  5232  axnul  5255  nalset  5263  notzfaus  5313  axpow3  5318  elALT2  5319  dtruALT2  5320  dvdemo1  5323  dvdemo2  5324  eusv2nf  5345  axprALT  5372  axprOLD  5381  exel  5388  dtruOLD  5396  inf1  9551  omex  9572  bnd  9821  axpowndlem2  10527  grothomex  10758  tgjustc1  28378  tgjustc2  28379  bnj101  34686  axsepg2  35045  axsepg2ALT  35046  axnulALT2  35056  axextdfeq  35758  ax8dfeq  35759  axextndbi  35765  snelsingles  35883  bj-ax6elem2  36628  ax6er  36794  bj-vtoclf  36876  wl-exeq  37495  exbiii  42171  sn-exelALT  42179  spd  49640  elpglem2  49674  eximp-surprise2  49747