Theorem eximii 1764

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

Syntax hints:   → wi 4  ∃wex 1704

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

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  exiftru  1891  spimeh  1925  ax6evr  1942  spimv1  2115  ax6e  2250  spim  2254  spimed  2255  spimv  2257  spei  2261  equvini  2346  equvel  2347  euequ1  2476  euex  2494  darii  2565  barbari  2567  festino  2571  baroco  2572  cesaro  2573  camestros  2574  datisi  2575  disamis  2576  felapton  2579  darapti  2580  dimatis  2582  fresison  2583  calemos  2584  fesapo  2585  bamalip  2586  vtoclf  3258  vtocl  3259  axrep2  4773  axnul  4788  nalset  4795  notzfaus  4840  el  4847  dtru  4857  eusv2nf  4864  dvdemo1  4902  dvdemo2  4903  axpr  4905  snnexOLD  6967  inf1  8519  bnd  8755  axpowndlem2  9420  grothomex  9651  bnj101  30789  axextdfeq  31703  ax8dfeq  31704  axextndbi  31710  snelsingles  32029  bj-ax6elem2  32652  bj-spimedv  32719  bj-spimvv  32721  bj-speiv  32724  bj-axrep2  32789  bj-nalset  32794  bj-el  32796  bj-dtru  32797  bj-dvdemo1  32802  bj-dvdemo2  32803  ax6er  32820  bj-vtoclf  32908  wl-exeq  33321  spd  42425  elpglem2  42455  eximp-surprise2  42531