Theorem eximii 1704

Description: Inference associated with eximi 1702. (Contributed by BJ, 3-Feb-2018.)

Hypotheses

Ref	Expression
eximii.1	|- E. x ph
eximii.2	|- ( ph -> ps )

Assertion

Ref	Expression
eximii	|- E. x ps

Proof of Theorem eximii

Step	Hyp	Ref	Expression
1		eximii.1	. 2 |- E. x ph
2		eximii.2	. . 3 |- ( ph -> ps )
3	2	eximi 1702	. 2 |- ( E. x ph -> E. x ps )
4	1, 3	ax-mp 5	1 |- E. x ps

Syntax hints:   -> wi 4   E.wex 1659

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

This theorem depends on definitions:  df-bi 188  df-ex 1660

This theorem is referenced by:  exiftru  1797  spimeh  1830  equidOLD  1841  cbv3hv  2012  ax6e  2056  spim  2060  spimed  2061  spei  2066  equvini  2142  equveli  2143  euequ1  2271  euex  2290  darii  2363  barbari  2365  festino  2369  baroco  2370  cesaro  2371  camestros  2372  datisi  2373  disamis  2374  felapton  2377  darapti  2378  dimatis  2380  fresison  2381  calemos  2382  fesapo  2383  bamalip  2384  vtoclf  3132  axrep2  4535  axnul  4550  nalset  4558  notzfaus  4596  el  4603  dtru  4612  eusv2nf  4619  dvdemo1  4653  dvdemo2  4654  axpr  4656  snnex  6608  inf1  8130  bnd  8365  axpowndlem2  9024  grothomex  9255  bnj101  29525  axextdfeq  30439  ax8dfeq  30440  axextndbi  30446  snelsingles  30682  bj-spimv  31267  bj-spimedv  31268  bj-speiv  31273  bj-axrep2  31362  bj-nalset  31367  bj-el  31369  bj-dtru  31370  bj-dvdemo1  31375  bj-dvdemo2  31376  ax6er  31393  bj-vtoclf  31472  wl-exeq  31781  eximp-surprise2  39798