Theorem eximii 1659

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

Syntax hints:   -> wi 4   E.wex 1613

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

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

This theorem is referenced by:  exiftru  1751  spimeh  1783  equid  1792  cbv3hv  1957  ax6e  2003  spim  2007  spimed  2008  spei  2013  equvini  2088  equveli  2089  equveliOLD  2090  euequ1  2289  euex  2309  darii  2398  barbari  2400  festino  2404  baroco  2405  cesaro  2406  camestros  2407  datisi  2408  disamis  2409  felapton  2412  darapti  2413  dimatis  2415  fresison  2416  calemos  2417  fesapo  2418  bamalip  2419  vtoclf  3160  axrep2  4570  nalset  4593  notzfaus  4631  el  4638  dtru  4647  eusv2nf  4654  dvdemo1  4691  dvdemo2  4692  axpr  4694  snnex  6605  inf1  8056  bnd  8327  axpowndlem2  8990  grothomex  9224  axextdfeq  29447  ax8dfeq  29448  axextndbi  29454  snelsingles  29777  wl-exeq  30192  eximp-surprise2  33344  bnj101  33919  bj-spimv  34422  bj-spimedv  34423  bj-speiv  34428  bj-axrep2  34518  bj-nalset  34523  bj-el  34525  bj-dtru  34526  bj-dvdemo1  34531  bj-dvdemo2  34532  ax6er  34549  bj-vtoclf  34623