Theorem eximii 1709

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

Syntax hints:   -> wi 4   E.wex 1663

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

This theorem depends on definitions:  df-bi 189  df-ex 1664

This theorem is referenced by:  exiftru  1808  spimeh  1841  equidOLD  1856  ax6evr  1859  spimv1  2058  cbv3hvOLD  2062  cbv3hvOLDOLD  2063  ax6e  2094  spim  2098  spimed  2099  spimv  2101  spei  2105  equvini  2179  equveli  2180  euequ1  2305  euex  2323  darii  2394  barbari  2396  festino  2400  baroco  2401  cesaro  2402  camestros  2403  datisi  2404  disamis  2405  felapton  2408  darapti  2409  dimatis  2411  fresison  2412  calemos  2413  fesapo  2414  bamalip  2415  vtoclf  3099  vtocl  3100  axrep2  4517  axnul  4532  nalset  4540  notzfaus  4578  el  4585  dtru  4594  eusv2nf  4601  dvdemo1  4635  dvdemo2  4636  axpr  4638  snnex  6597  inf1  8127  bnd  8363  axpowndlem2  9023  grothomex  9254  bnj101  29529  axextdfeq  30444  ax8dfeq  30445  axextndbi  30451  snelsingles  30689  bj-ax6elem2  31265  bj-spimedv  31320  bj-spimvv  31322  bj-speiv  31325  bj-axrep2  31404  bj-nalset  31409  bj-el  31411  bj-dtru  31412  bj-dvdemo1  31417  bj-dvdemo2  31418  ax6er  31435  bj-vtoclf  31515  wl-exeq  31867  eximp-surprise2  40577