Theorem eximii 1717

Description: Inference associated with eximi 1715. (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 1715	. 2 |- ( E. x ph -> E. x ps )
4	1, 3	ax-mp 5	1 |- E. x ps

Syntax hints:   -> wi 4   E.wex 1671

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

This theorem depends on definitions:  df-bi 190  df-ex 1672

This theorem is referenced by:  exiftru  1816  spimeh  1849  equidOLD  1864  ax6evr  1867  spimv1  2077  cbv3hvOLD  2081  cbv3hvOLDOLD  2082  ax6e  2107  spim  2111  spimed  2112  spimv  2114  spei  2118  equvini  2195  equveli  2196  euequ1  2325  euex  2343  darii  2414  barbari  2416  festino  2420  baroco  2421  cesaro  2422  camestros  2423  datisi  2424  disamis  2425  felapton  2428  darapti  2429  dimatis  2431  fresison  2432  calemos  2433  fesapo  2434  bamalip  2435  vtoclf  3085  vtocl  3086  axrep2  4510  axnul  4525  nalset  4533  notzfaus  4576  el  4583  dtru  4592  eusv2nf  4599  dvdemo1  4635  dvdemo2  4636  axpr  4638  snnex  6616  inf1  8145  bnd  8381  axpowndlem2  9041  grothomex  9272  bnj101  29601  axextdfeq  30515  ax8dfeq  30516  axextndbi  30522  snelsingles  30760  bj-ax6elem2  31329  bj-spimedv  31386  bj-spimvv  31388  bj-speiv  31391  bj-axrep2  31470  bj-nalset  31475  bj-el  31477  bj-dtru  31478  bj-dvdemo1  31483  bj-dvdemo2  31484  ax6er  31501  bj-vtoclf  31583  wl-exeq  31937  eximp-surprise2  41030