Theorem eximii 1626

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

Syntax hints:   -> wi 4   E.wex 1516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  spimfv  1723  ax6evr  1729  spimed  1764  darii  2156  barbari  2158  festino  2162  baroco  2163  cesaro  2164  camestros  2165  datisi  2166  disamis  2167  felapton  2170  darapti  2171  dimatis  2173  fresison  2174  calemos  2175  fesapo  2176  bamalip  2177  ceqsexv2d  2817  vtoclf  2831  vtocl2  2833  vtocl3  2834  nalset  4190  el  4238  dtruarb  4251  snnex  4513  eusv2nf  4521  dtruex  4625  limom  4680  nninfct  12477  bj-axemptylem  16027  bj-nalset  16030  bj-d0clsepcl  16060  bj-omex2  16112  bj-nn0sucALT  16113