Theorem eximii 1590

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

Syntax hints:   -> wi 4   E.wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-ial 1522

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  spimfv  1687  ax6evr  1693  spimed  1728  darii  2114  barbari  2116  festino  2120  baroco  2121  cesaro  2122  camestros  2123  datisi  2124  disamis  2125  felapton  2128  darapti  2129  dimatis  2131  fresison  2132  calemos  2133  fesapo  2134  bamalip  2135  vtoclf  2779  vtocl2  2781  vtocl3  2782  nalset  4112  el  4157  dtruarb  4170  snnex  4426  eusv2nf  4434  dtruex  4536  limom  4591  bj-axemptylem  13774  bj-nalset  13777  bj-d0clsepcl  13807  bj-omex2  13859  bj-nn0sucALT  13860