Theorem eximii 1679

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

Syntax hints:   -> wi 4   E.wex 1633

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

This theorem depends on definitions:  df-bi 185  df-ex 1634

This theorem is referenced by:  exiftru  1774  spimeh  1806  equid  1815  cbv3hv  1984  ax6e  2029  spim  2033  spimed  2034  spei  2039  equvini  2113  equveli  2114  euequ1  2244  euex  2264  darii  2343  barbari  2345  festino  2349  baroco  2350  cesaro  2351  camestros  2352  datisi  2353  disamis  2354  felapton  2357  darapti  2358  dimatis  2360  fresison  2361  calemos  2362  fesapo  2363  bamalip  2364  vtoclf  3110  axrep2  4509  nalset  4531  notzfaus  4569  el  4576  dtru  4585  eusv2nf  4592  dvdemo1  4626  dvdemo2  4627  axpr  4629  snnex  6588  inf1  8072  bnd  8342  axpowndlem2  9005  grothomex  9237  bnj101  29103  axextdfeq  30017  ax8dfeq  30018  axextndbi  30024  snelsingles  30260  bj-spimv  30843  bj-spimedv  30844  bj-speiv  30849  bj-axrep2  30939  bj-nalset  30944  bj-el  30946  bj-dtru  30947  bj-dvdemo1  30952  bj-dvdemo2  30953  ax6er  30970  bj-vtoclf  31044  wl-exeq  31354  eximp-surprise2  38844