Theorem eximii 1625

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

Syntax hints:   -> wi 4   E.wex 1515

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-ial 1557

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  spimfv  1722  ax6evr  1728  spimed  1763  darii  2154  barbari  2156  festino  2160  baroco  2161  cesaro  2162  camestros  2163  datisi  2164  disamis  2165  felapton  2168  darapti  2169  dimatis  2171  fresison  2172  calemos  2173  fesapo  2174  bamalip  2175  ceqsexv2d  2812  vtoclf  2826  vtocl2  2828  vtocl3  2829  nalset  4174  el  4222  dtruarb  4235  snnex  4495  eusv2nf  4503  dtruex  4607  limom  4662  nninfct  12362  bj-axemptylem  15828  bj-nalset  15831  bj-d0clsepcl  15861  bj-omex2  15913  bj-nn0sucALT  15914