Theorem eximii 1637

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

Syntax hints:   -> wi 4   E.wex 1596

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

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

This theorem is referenced by:  exiftru  1722  spimeh  1731  equid  1740  cbv3hv  1903  ax6e  1971  spim  1975  spimed  1976  spei  1981  equvini  2060  equveli  2061  equveliOLD  2062  2ax6elem  2179  euequ1  2281  euex  2303  darii  2408  barbari  2410  festino  2414  baroco  2415  cesaro  2416  camestros  2417  datisi  2418  disamis  2419  felapton  2422  darapti  2423  dimatis  2425  fresison  2426  calemos  2427  fesapo  2428  bamalip  2429  vtoclf  3169  axrep2  4566  nalset  4590  notzfaus  4628  el  4635  dtru  4644  eusv2nf  4651  dvdemo1  4688  dvdemo2  4689  axpr  4691  snnex  6601  inf1  8051  bnd  8322  grothomex  9219  axextdfeq  29157  ax8dfeq  29158  axextndbi  29164  snelsingles  29499  wl-exeq  29914  eximp-surprise2  32682  bnj101  33257  bj-spimv  33762  bj-spimedv  33763  bj-speiv  33768  bj-axrep2  33857  bj-nalset  33862  bj-el  33864  bj-dtru  33865  bj-dvdemo1  33870  bj-dvdemo2  33871  ax6er  33888  bj-vtoclf  33962